diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy index 33d49f2f..8d4a563f 100755 --- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy @@ -1109,10 +1109,17 @@ thm "thm111" section\Toplevel --- aka. ''The Isar Engine''\ -text\The main structure of the Isar-engine is \<^ML_structure>\Toplevel\ and provides and -internal \<^ML_type>\state\ with the necessary infrastructure --- -i.e. the operations to pack and unpack theories and \<^ML_type>\Proof.context\'s --- on it: - +text\ The main structure of the Isar-engine is \<^ML_structure>\Toplevel\. + The Isar Toplevel (aka "the Isar engine" or the "Isar Interpreter") is an transaction + machine sitting over the Isabelle Kernel steering some asynchronous evaluation during the + evaluation of Isabelle/Isar input, usually stemming from processing Isabelle \<^verbatim>\.thy\-files. \ + +subsection*[tplstate::technical] \Toplevel Transaction Management in the Isar-Engine\ +text\ + The structure \<^ML_structure>\Toplevel\ provides and internal \<^ML_type>\state\ with the + necessary infrastructure --- i.e. the operations to pack and unpack theories and + queries on it: + \<^item> \<^ML>\ Toplevel.theory_toplevel: theory -> Toplevel.state\ \<^item> \<^ML>\ Toplevel.init_toplevel: unit -> Toplevel.state\ \<^item> \<^ML>\ Toplevel.is_toplevel: Toplevel.state -> bool\ @@ -1121,209 +1128,169 @@ i.e. the operations to pack and unpack theories and \<^ML_type>\Proof.con \<^item> \<^ML>\ Toplevel.is_skipped_proof: Toplevel.state -> bool\ \<^item> \<^ML>\ Toplevel.level: Toplevel.state -> int\ \<^item> \<^ML>\ Toplevel.context_of: Toplevel.state -> Proof.context\ + extracts the local context \<^item> \<^ML>\ Toplevel.generic_theory_of: Toplevel.state -> generic_theory\ + extracts the generic (local or global) context \<^item> \<^ML>\ Toplevel.theory_of: Toplevel.state -> theory\ + extracts the global context \<^item> \<^ML>\ Toplevel.proof_of: Toplevel.state -> Proof.state\ \<^item> \<^ML>\ Toplevel.presentation_context: Toplevel.state -> Proof.context\ \<^item> ... \ +text\ Type \<^ML_type>\Toplevel.state\ represents Isar toplevel states, which are normally + manipulated through the concept of toplevel transitions only. + This type is constructed as the sum of \<^emph>\empty state\, \<^ML_type>\Context.generic\ + (synonym to \<^ML_type>\generic_theory\) and enriched versions of proof states or + abort proofs. +\ + + +subsection*[transmgt::technical] \Toplevel Transaction Management in the Isar-Engine\ + text\ The extensibility of Isabelle as a system framework depends on a number of tables, into which various concepts commands, ML-antiquotations, text-antiquotations, cartouches, ... can be entered via a late-binding on the fly. - A paradigmatic example is the \<^ML>\Outer_Syntax.command\-operation, which --- - representing in itself a toplevel system transition --- allows to define a new - command section and bind its syntax and semantics at a specific keyword. - Calling \<^ML>\Outer_Syntax.command\ - creates an implicit \<^ML>\Theory.setup\ with an entry for a call-back function, which happens - to be a parser that must have as side-effect a Toplevel-transition-transition. - Registers \<^ML_type>\Toplevel.transition -> Toplevel.transition\ parsers to the - Isar interpreter. + The main operations to toplevel transitions are: + + \<^item> \<^ML>\Toplevel.keep: (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition\ + adjoins a diagnostic command + \<^item> \<^ML>\Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition\ + adjoins a theory transformer. + \<^item> \<^ML>\Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition\ + \<^item> \<^ML>\Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition\ + \<^item> \<^ML>\Toplevel.exit: Toplevel.transition -> Toplevel.transition\ + \<^item> \<^ML>\Toplevel.ignored: Position.T -> Toplevel.transition\ + \<^item> \<^ML>\Toplevel.present_local_theory: (xstring * Position.T) option -> + (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition\ - The global type of this key function for extending the Isar toplevel is, together - with a few query operations on the state of the toplevel: - \<^item> \<^ML>\Outer_Syntax.command : Outer_Syntax.command_keyword -> string -> - (Toplevel.transition -> Toplevel.transition) parser -> unit\, - \<^item> \<^ML>\Document.state : unit -> Document.state\, giving the state as a "collection of named - nodes, each consisting of an editable list of commands, associated with asynchronous - execution process, - \<^item> \<^ML>\Session.get_keywords : unit -> Keyword.keywords\, this looks to be session global, - \<^item> \<^ML>\Thy_Header.get_keywords : theory -> Keyword.keywords\ this looks to be just theory global. - \ +subsection*[cmdbinding::technical] \Toplevel Transaction Management in the Isar-Engine\ +text\ + Toplevel transitions can finally be registered together with commandkeywords and + IDE information into the toplevel. + The global type of this key function for extending the Isar toplevel is, together + with a few query operations on the state of the toplevel: + \<^item> \<^ML>\Outer_Syntax.command : Outer_Syntax.command_keyword -> string -> + (Toplevel.transition -> Toplevel.transition) parser -> unit\, + \<^item> \<^ML>\Document.state : unit -> Document.state\, giving the state as a "collection of named + nodes, each consisting of an editable list of commands, associated with asynchronous + execution process, + \<^item> \<^ML>\Session.get_keywords : unit -> Keyword.keywords\, this looks to be session global, + \<^item> \<^ML>\Thy_Header.get_keywords : theory -> Keyword.keywords\ this looks to be just theory global. + A paradigmatic example is the \<^ML>\Outer_Syntax.command\-operation, which --- + representing itself as a toplevel system transition --- allows to define a new + command section and bind its syntax and semantics at a specific keyword. + Calling \<^ML>\Outer_Syntax.command\ creates an implicit \<^ML>\Theory.setup\ with an entry + for a call-back function, which happens to be a parser that must have as side-effect + a Toplevel-transition-transition. + Registers \<^ML_type>\Toplevel.transition -> Toplevel.transition\ parsers to the + Isar interpreter.\ + +text\The file \<^file>\~~/src/HOL/ex/Commands.thy\ shows some example Isar command definitions, with the + all-important theory header declarations for outer syntax keywords.\ + subsubsection*[ex1137::example]\Examples: \<^theory_text>\text\\ -text\ +text\ The integration of the \<^theory_text>\text\-command is done as follows: + @{ML [display]\ Outer_Syntax.command ("text", @{here}) "formal comment (primary style)" (Parse.opt_target -- Parse.document_source >> Pure_Syn.document_command {markdown = true}) \} + + where \<^ML>\Pure_Syn.document_command\ is the defining operation for the + "diagnostic" (=side-effect-free) toplevel operation \<^ML>\Pure_Syn.document_command\ looks as follows: + + @{ML [display]\ let fun output_document state markdown txt = + Thy_Output.output_document (Toplevel.presentation_context state) markdown txt + fun document_command markdown (loc, txt) = + Toplevel.keep (fn state => + (case loc of + NONE => ignore (output_document state markdown txt) + | SOME (_, pos) => + error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o + Toplevel.present_local_theory loc (fn state => + ignore (output_document state markdown txt)) in () end + +\} + \ +subsubsection*[ex1138::example]\Examples: \<^theory_text>\ML\\ + +text\ + The integration of the \<^theory_text>\ML\-command is done as follows: + + @{ML [display]\ + Outer_Syntax.command ("ML", \<^here>) "ML text within theory or local theory" + (Parse.ML_source >> (fn source => + Toplevel.generic_theory + (ML_Context.exec (fn () => + ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source) #> + Local_Theory.propagate_ml_env))) + \} +\ + + +subsection\Miscellaneous\ text\Here are a few queries relevant for the global config of the isar engine:\ ML\ Document.state();\ ML\ Session.get_keywords(); (* this looks to be session global. *) \ ML\ Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \ - - -subsection*[transmgt::technical] \Transaction Management in the Isar-Engine : The Toplevel \ -text\ The Isar Toplevel (aka "the Isar engine" or the "Isar Interpreter") is an transaction - machine sitting over the Isabelle Kernel steering some asynchronous evaluation during the - evaluation of Isabelle/Isar input, usually stemming from processing Isabelle \<^verbatim>\.thy\-files. - -\ - -text\ -\<^enum> Type \<^ML_type>\Toplevel.state\ represents Isar toplevel states, which are normally - manipulated through the concept of toplevel transitions only. - This type is constructed as the sum of \<^emph>\empty state\, \<^ML_type>\Context.generic\ - (synonym to \<^ML_type>\generic_theory\) and - -TODO XXL - -\ - - -ML\Toplevel.exit: Toplevel.transition -> Toplevel.transition; - Toplevel.keep: (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; - Toplevel.keep': (bool -> Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; - Toplevel.ignored: Position.T -> Toplevel.transition; - Toplevel.generic_theory: (generic_theory -> generic_theory) -> Toplevel.transition -> Toplevel.transition; - Toplevel.theory': (bool -> theory -> theory) -> Toplevel.transition -> Toplevel.transition; - Toplevel.theory: (theory -> theory) -> Toplevel.transition -> Toplevel.transition; - Toplevel.present_local_theory: - (xstring * Position.T) option -> - (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; - (* where text treatment and antiquotation parsing happens *) - - - (*fun document_command markdown (loc, txt) = - Toplevel.keep (fn state => - (case loc of - NONE => ignore (output_text state markdown txt) - | SOME (_, pos) => - error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o - Toplevel.present_local_theory loc (fn state => ignore (output_text state markdown txt)); *) - - (* Isar Toplevel Steuerung *) - Toplevel.keep : (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; - (* val keep' = add_trans o Keep; - fun keep f = add_trans (Keep (fn _ => f)); - *) - - Toplevel.present_local_theory : (xstring * Position.T) option -> (Toplevel.state -> unit) -> - Toplevel.transition -> Toplevel.transition; - (* fun present_local_theory target = present_transaction (fn int => - (fn Theory (gthy, _) => - let val (finish, lthy) = Named_Target.switch target gthy; - in Theory (finish lthy, SOME lthy) end - | _ => raise UNDEF)); - - fun present_transaction f g = add_trans (Transaction (f, g)); - fun transaction f = present_transaction f (K ()); - *) - - Toplevel.theory : (theory -> theory) -> Toplevel.transition -> Toplevel.transition; - (* fun theory' f = transaction (fn int => - (fn Theory (Context.Theory thy, _) => - let val thy' = thy - |> Sign.new_group - |> f int - |> Sign.reset_group; - in Theory (Context.Theory thy', NONE) end - | _ => raise UNDEF)); - - fun theory f = theory' (K f); *)\ - - -ML\ - -(* Isar Toplevel Control *) -Toplevel.keep : (Toplevel.state -> unit) -> Toplevel.transition -> Toplevel.transition; - (* val keep' = add_trans o Keep; - fun keep f = add_trans (Keep (fn _ => f)); - *) - -Toplevel.present_local_theory : (xstring * Position.T) option -> (Toplevel.state -> unit) -> - Toplevel.transition -> Toplevel.transition; - (* fun present_local_theory target = present_transaction (fn int => - (fn Theory (gthy, _) => - let val (finish, lthy) = Named_Target.switch target gthy; - in Theory (finish lthy, SOME lthy) end - | _ => raise UNDEF)); - - fun present_transaction f g = add_trans (Transaction (f, g)); - fun transaction f = present_transaction f (K ()); - *) - -Toplevel.theory : (theory -> theory) -> Toplevel.transition -> Toplevel.transition; - (* fun theory' f = transaction (fn int => - (fn Theory (Context.Theory thy, _) => - let val thy' = thy - |> Sign.new_group - |> f int - |> Sign.reset_group; - in Theory (Context.Theory thy', NONE) end - | _ => raise UNDEF)); - - fun theory f = theory' (K f); *) -\ - - -subsection*[conf::technical]\ Configuration flags of fixed type in the Isar-engine. \ +subsection*[conf::technical]\ Configuration Flags in the Isar-engine. \ text\The toplevel also provides an infrastructure for managing configuration options for system components. Based on a sum-type @{ML_type Config.value } with the alternatives \<^verbatim>\ Bool of bool | Int of int | Real of real | String of string\ and building the parametric configuration types @{ML_type "'a Config.T" } and the - instance \<^verbatim>\type raw = value T\, for all registered configurations the protocol:\ -ML\ + instance \<^verbatim>\type raw = value T\, for all registered configurations the protocol: - Config.get: Proof.context -> 'a Config.T -> 'a; - Config.map: 'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context; - Config.put: 'a Config.T -> 'a -> Proof.context -> Proof.context; - Config.get_global: theory -> 'a Config.T -> 'a; - Config.map_global: 'a Config.T -> ('a -> 'a) -> theory -> theory; - Config.put_global: 'a Config.T -> 'a -> theory -> theory;\ -text\... etc. is defined.\ + \<^item> \<^ML>\Config.get : Proof.context -> 'a Config.T -> 'a\ + \<^item> \<^ML>\Config.map: 'a Config.T -> ('a -> 'a) -> Proof.context -> Proof.context\ + \<^item> \<^ML>\Config.put: 'a Config.T -> 'a -> Proof.context -> Proof.context\ + \<^item> \<^ML>\Config.get_global: theory -> 'a Config.T -> 'a\ + \<^item> \<^ML>\Config.map_global: 'a Config.T -> ('a -> 'a) -> theory -> theory\ + \<^item> \<^ML>\Config.put_global: 'a Config.T -> 'a -> theory -> theory\ + \<^item> ... etc. is defined. +\ -subsubsection*[ex::example]\Example registration of an config attribute XS232 initialized to false: \ -ML\ + +subsubsection*[ex::example]\Example registration of an config attribute \ +text\The attribute XS232 is initialized by false:\ +ML\ val (XS232, XS232_setup) = Attrib.config_bool \<^binding>\XS232\ (K false); val _ = Theory.setup XS232_setup;\ -(* or: just command: +text \... which could also be achieved by \setup\XS232_setup\\. \ -setup\XS232_setup\ - -*) - -text\Defining a high-level attribute:\ +subsubsection*[ex33333::example]\Defining a high-level attribute:\ ML\ Attrib.setup \<^binding>\simp\ (Attrib.add_del Simplifier.simp_add Simplifier.simp_del) "declaration of Simplifier rewrite rule" \ - +subsection*[ex333::example]\A Hack:\ text\Another mechanism are global synchronised variables:\ -ML\ (* For example *) +ML\ val C = Synchronized.var "Pretty.modes" "latEEex"; (* Synchronized: a mechanism to bookkeep global variables with synchronization mechanism included *) Synchronized.value C;\ -subsection*[ex213::example]\A Definition (High-level)\ -text\Example drawn from theory \<^verbatim>\Clean\:\ +subsection*[ex213::example]\A Definition Command (High-level)\ + +text\A quite complex example is drawn from the Theory \<^verbatim>\Clean\; it generates \ ML\ structure HLDefinitionSample = @@ -1398,15 +1365,9 @@ fun lemma1' lemma_name goals_to_prove a b lthy = \ -text\MORE TO COME\ - - - - - chapter*[frontend::technical]\Front-End \ text\In the following chapter, we turn to the right part of the system architecture - shown in @{docitem \architecture\}: + shown in \<^figure>\architecture\: The PIDE ("Prover-IDE") layer @{cite "DBLP:conf/itp/Wenzel14"} consisting of a part written in SML and another in SCALA. Roughly speaking, PIDE implements "continuous build - continuous check" - functionality @@ -1423,6 +1384,7 @@ text\In the following chapter, we turn to the right part of the system arc extent (outdated markup referring to modified text is dropped, and corresponding re-calculations are oriented to the user focus, for example). Four concrete editors --- also called PIDE applications --- have been implemented: + \<^enum> an Eclipse plugin (developped by an Edinburg-group, based on an very old PIDE version), \<^enum> a Visual-Studio Code plugin (developed by Makarius Wenzel), currently based on a fairly old PIDE version,