Theory 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 (name, (source, pos)) =
      ML_Context.expression pos
        (ML_Lex.read "val" @ name @ ML_Lex.read "= Context.>>> (" @ source @ ML_Lex.read ")")
    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 >> (setup_result #> Context.theory_map #> Toplevel.theory));
    Outer_Syntax.local_theory \<^command_keyword>‹local_setup_result›
      "ML setup with result for local theory"
      (parse >> (setup_result #> K #>
        Local_Theory.declaration {pos = ⌂, syntax = false, pervasive = false}))
  end
›

end