Theory ML_Unification.Setup_Result_Commands

✐‹creator "Kevin Kappelmann"›
subsection ‹Setup Result Commands›
theory Setup_Result_Commands
  imports Pure
  keywords "setup_result" :: thy_decl
  and "local_setup_result" :: thy_decl
begin

paragraph ‹Summary›
text ‹Setup and local setup with result commands›

ML‹
  let
    fun setup_result finish (name, (source, pos)) =
      ML_Context.expression pos
        (ML_Lex.read "val" @ name @ ML_Lex.read "= Context.>>> (" @ source @ ML_Lex.read ")")
      |> finish
    val parse = Parse.embedded_ml
      -- ((\<^keyword>‹=› || \<^keyword>‹≡›)
      |-- Parse.position Parse.embedded_ml)
  in
    Outer_Syntax.command \<^command_keyword>‹setup_result›
      "ML setup with result for global theory"
      (parse >> (Toplevel.theory o setup_result Context.theory_map));
    Outer_Syntax.local_theory \<^command_keyword>‹local_setup_result›
      "ML setup with result for local theory"
      (parse >> (setup_result
        (Local_Theory.declaration {pos = ⌂, syntax = false, pervasive = false} o K)))
  end
›

end