Isabelle/export/parser.ml

	parser.ml revision 18d5da8101a438aaf8c27d7e740f835e707fc0b8
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersignature ParserHelper =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersig
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    type thy_body
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    val cmd_theory : (Token.T list * Thy_Header.header) parser
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    val cmd_header : string parser
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    val thy_body : (Token.T list * thy_body) parser
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    val unparse_tokens : Token.T list -> string
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    val init_thy : (Token.T list * Thy_Header.header) ->
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                       Toplevel.state * (Toplevel.state ->
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                        Token.T list -> Toplevel.state)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederend;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederstructure ParserHelper : ParserHelper =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederstruct
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    type opt_target = (xstring * Position.T) option;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    datatype misc_body = Chapter of opt_target * string
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                            |Section of opt_target * string
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                            |Subsection of opt_target * string
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                            |Subsubsection of opt_target * string
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                            |Text of opt_target * string
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                            |TextRaw of opt_target * string
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                            |Sect of string
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                            |Subsect of string
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                            |Subsubsect of string
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                            |Txt of string
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                            |TxtRaw of string
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                |DiagnosticCommand of string
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                            |TopLevelCommand of string;
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    type proof = string;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    type ml_text = string * Position.T;
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    type orig = Token.T list;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    (* isar-ref.pdf page 78 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    datatype context_head = ContextNamed of xstring * Position.T
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                               |ContextHead  of ((xstring * Position.T) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                                                * Element.context list);
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    datatype instance_type = InstanceArity of string list * string list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                                                 *string
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                                |InstanceSubset of string;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    datatype thy_body =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder         Classes of (binding * string list) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |Classrel of (string * string) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |DefaultSort of opt_target * string
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |TypeDecl of ((opt_target * string list) * binding) * mixfix
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |TypeSynonym of ((opt_target * string list) * binding) *
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                        (string * mixfix)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |Nonterminal of binding list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |Arities of (string * string list * string) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |Judgement of (binding * string * mixfix)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Consts of (binding * string * mixfix) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Syntax of (string * bool) * (string * string * mixfix) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |NoSyntax of (string * bool) * (string * string * mixfix) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |Translations of (xstring * string) Syntax.trrule list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |NoTranslations of (xstring * string) Syntax.trrule list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |Axioms of (Attrib.binding * string) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Defs of (bool * bool) * ((binding * string) * Args.src list) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |Definition of opt_target * ((binding * string option * mixfix) option
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       * (Attrib.binding * string))
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Abbreviation of opt_target * ((string * bool) *
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                          ((binding * string option * mixfix) option * string))
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |TypeNotation of opt_target * ((string * bool) * (string * mixfix) list)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |NoTypeNotation of opt_target * ((string * bool) *
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                                         (string * mixfix) list)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |Notation of opt_target * ((string * bool) * (string * mixfix) list)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |NoNotation of opt_target * ((string * bool) * (string * mixfix) list)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |Axiomatization of (binding * string option * mixfix) list *
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                           (Attrib.binding * string list) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Theorems of (opt_target * (Attrib.binding *
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      (Facts.ref * Args.src list) list) list) *
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                     (binding * string option * mixfix) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Lemmas of (opt_target * (Attrib.binding *
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      (Facts.ref * Args.src list) list) list) *
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                     (binding * string option * mixfix) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Declare of (opt_target * (Facts.ref * Args.src list) list list) *
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                    (binding * string option * mixfix) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Hide of string * (bool * xstring list)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Use of string
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |ML of ml_text
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |ML_prf of ml_text
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |ML_val of ml_text
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |ML_command of ml_text
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |Setup of ml_text
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |LocalSetup of opt_target * ml_text
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |AttributeSetup of (bstring * Position.T) * (ml_text * string)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |MethodSetup of (bstring * Position.T) * (ml_text * string)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Declaration of (opt_target * bool) * ml_text
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |SyntaxDeclaration of (opt_target * bool) * ml_text
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |SimprocSetup of (((opt_target * (bstring * Position.T)) *
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                           string list) * ml_text) * xstring list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |ParseAstTranslation of bool * (string * Position.T)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |ParseTranslation of bool * (string * Position.T)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |PrintTranslation of bool * (string * Position.T)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |TypedPrintTranslation of bool * (string * Position.T)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |PrintAstTranslation of bool * (string * Position.T)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Oracle of (bstring * Position.T) * ml_text
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Bundle of ((opt_target * binding) * (Facts.ref * Args.src list) list) *
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                    (binding * string option * mixfix) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Include of (xstring * Position.T) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Including of (xstring * Position.T) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |PrintBundles
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    |Context of context_head * (orig * thy_body) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Locale of (binding * (Expression.expression * Element.context list))
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                   * (orig * thy_body) list
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    |Sublocale of ((xstring * Position.T) * (Expression.expression *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                        (Attrib.binding * string) list)) * proof
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    |Interpretation of (Expression.expression *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                            (Attrib.binding * string) list) * proof
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        |Interpret of Expression.expression *
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      (Attrib.binding * string) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    |Class of (binding * (string list * Element.context list)) *
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                  (orig * thy_body) list
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    |Subclass of string * proof
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    |Instantiation of (string list * string list * string) *
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                          (orig * thy_body) list
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    |Instance of ((string * instance_type) option) * proof
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    |Overloading of (bstring * string * bool) list * (orig * thy_body) list
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    |Theorem of (((opt_target * Attrib.binding) *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                      (xstring * Position.T) list) *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                     (Element.context list * Element.statement)) * proof
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    |Lemma of (((opt_target * Attrib.binding) *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                    (xstring * Position.T) list) *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                   (Element.context list * Element.statement)) * proof
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    |Corollary of (((opt_target * Attrib.binding) *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                        (xstring * Position.T) list) *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                       (Element.context list * Element.statement)) * proof
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    |SchematicTheorem of (((opt_target * Attrib.binding) *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                               (xstring * Position.T) list) *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                              (Element.context list * Element.statement)) *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                             proof
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder        |SchematicLemma of (((opt_target * Attrib.binding) *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                             (xstring * Position.T) list) *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                            (Element.context list * Element.statement)) * proof
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder        |SchematicCorollary of (((opt_target * Attrib.binding) *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                                 (xstring * Position.T) list) *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                                (Element.context list * Element.statement)) *
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                               proof
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder    |Primrec of (opt_target * (binding * string option * mixfix) list) *
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder                    (Attrib.binding * string) list
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder    |Datatype of Datatype.spec_cmd list
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder    |RepDatatype of string list
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder    |Fun of ((Function_Common.function_config * (binding *
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder                 string option * mixfix) list) *
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder                (Attrib.binding * string) list)
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder        |PartialFunction of xstring * ((binding * string option * mixfix) list *
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder                             (Attrib.binding  * string))
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder    |Function of ((Function_Common.function_config *
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder                       (binding * string option * mixfix) list)
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder                      * (Attrib.binding * string) list) * proof
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder    |Termination of string option * proof
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder    |Misc of misc_body;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    val hide = curry Hide;
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    fun preserve_toks f toks =
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder             let val (v,toks') = f toks
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                 val consumed_toks = List.take(toks,List.length toks-
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                                                    List.length toks')
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder             in ((consumed_toks,v),toks') end;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(* Common Functions *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    (* taken from Pure/Isar/parse.ML *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    fun RESET_VALUE atom =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          Scan.ahead (Scan.one (K true)) -- atom >>
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder           (fn (arg, x) => (Token.assign NONE arg; x));
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder        fun token p = RESET_VALUE (Scan.one p);
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    fun unparse_kind k = Parse.group (fn () => Token.str_of_kind k)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder             (token (Token.is_kind k) >> Token.unparse);
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        val unparse_verbatim = unparse_kind Token.Verbatim;
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    val not_command = Parse.group (fn () => "non-command token")
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder             (token (not o Token.is_command));
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    fun command s = Parse.group (fn () => "command "^s)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder             (token (fn t => Token.is_command t andalso
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                             Token.content_of t = s));
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    fun command_with_args s = command s -- Scan.repeat not_command >> op::;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(* Pure/pure_syn.ML *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    (* line 12 *)
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder        val cmd_theory = preserve_toks (Parse.command_name "theory"
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                          |-- Thy_Header.args);
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder(* Pure/Isar/isar_syn.ML *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    (* line 14 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        val cmd_header = Parse.command_name "header" |-- unparse_verbatim;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    (* line 133 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    val opt_mode =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          (* line 129 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          let val mode_spec = (@{keyword "output"} >> K ("", false)) ||
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                              Parse.name -- Scan.optional
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                               (@{keyword "output"} >> K false) true;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          in Scan.optional (@{keyword "("} |-- Parse.!!!
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder              (mode_spec --| @{keyword ")"})) Syntax.mode_default end;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    val trans_line = (* line 157 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          let val trans_pat = (* line 147 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                   Scan.optional
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                    (@{keyword "("} |-- Parse.!!!
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                     (Parse.xname --| @{keyword ")"}))
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                    "logic" -- Parse.inner_syntax Parse.string
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder              fun trans_arrow toks = (* line 152 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                  ((@{keyword "\<rightharpoonup>"} || @{keyword "=>"})
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                   >> K Syntax.Parse_Rule ||
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                  (@{keyword "\<leftharpoondown>"} || @{keyword "<="})
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                   >> K Syntax.Print_Rule ||
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                  (@{keyword "\<rightleftharpoons>"} || @{keyword "=="})
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                   >> K Syntax.Parse_Print_Rule) toks
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder      in trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        >> (fn (left, (arr, right)) => arr (left, right)) end;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    fun first' l = Scan.first (List.map preserve_toks l);
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    fun parse_interpretation_arguments mandatory = (* line 428 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder      Parse.!!! (Parse_Spec.locale_expression mandatory) --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        Scan.optional
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          (Parse.where_ |-- Parse.and_list1
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder               (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    (* line 514 *)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    val parse_theorem = Parse.opt_target --
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder             Scan.optional (Parse_Spec.opt_thm_name ":" --|
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder             Scan.ahead (Parse_Spec.includes >> K "" ||
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder             Parse_Spec.locale_keyword ||
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder             Parse_Spec.statement_keyword)) Attrib.empty_binding --
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder             Scan.optional Parse_Spec.includes [] --
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder             Parse_Spec.general_statement;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    val mk_thy_body = List.map (fn (s,p) => Parse.command_name s |-- p);
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    fun partition p [] = []
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder           |partition p (t::l')  = let val (cmd,l'') = take_prefix p l'
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                                   in (t::cmd)::(partition p l'') end;
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    fun proof_qed i = Parse.group (fn () => "proof_qed")
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                          (fn t =>
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                           if i > 0 then Scan.first
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                                    [command "qed" -- proof_qed (i-1) >> op::,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                                     command "oops" >> single,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                                     command_with_args "proof"
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                                      -- proof_qed (i+1) >> op@,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                                     (token Token.is_command --
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                                      Scan.repeat not_command >> op::)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                                     -- proof_qed i >> op@] t
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                           else ([],t));
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    val proof_prefix = Scan.repeat (Scan.first
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                            [command_with_args "apply",
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                             command_with_args "using",
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                             command_with_args "unfolding"]) >> flat;
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    val unparse_tokens = (List.map (List.map Token.unparse)
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                         #> List.map (space_implode " ")
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                         #> cat_lines) o (partition Token.is_command);
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    val proof = Parse.!!! ((proof_prefix -- Scan.first
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                      [command_with_args "proof" -- proof_qed 1 >> op@,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                       command "oops" >> single,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                       command_with_args "by",
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                       command ".." >> single,
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                       command "." >> single]) >> op@
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                     >> unparse_tokens);
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    val simple_thy_body' = first' (mk_thy_body [
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("chapter", Parse.opt_target -- unparse_verbatim
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                     >> (Misc o Chapter)),                 (* line 19 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("section", Parse.opt_target -- unparse_verbatim
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                     >> (Misc o Section)),                 (* line 24 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("subsection", Parse.opt_target -- unparse_verbatim
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                        >> (Misc o Subsection)),           (* line 29 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("subsubsection", Parse.opt_target -- unparse_verbatim
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                           >> (Misc o Subsubsection)),     (* line 34 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("text", Parse.opt_target -- unparse_verbatim
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                  >> (Misc o Text)),                       (* line 39 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("text_raw", Parse.opt_target -- unparse_verbatim
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      >> (Misc o Text)),                   (* line 44 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("sect", unparse_verbatim >> (Misc o Sect)),       (* line 49 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("subsect", unparse_verbatim >> (Misc o Sect)),    (* line 54 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("subsubsect", unparse_verbatim
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                        >> (Misc o Subsubsect)),           (* line 59 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("txt", unparse_verbatim >> (Misc o Txt)),         (* line 64 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("txt_raw", unparse_verbatim >> (Misc o TxtRaw)),  (* line 69 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("classes",Scan.repeat1 (Parse.binding --          (* line 79 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                    Scan.optional ((@{keyword "\<subseteq>"}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                     || @{keyword "<"}) |-- Parse.!!!
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                    (Parse.list1 Parse.class)) []) >> Classes),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("classrel",Parse.and_list1 (Parse.class --        (* line 85 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                     ((@{keyword "\<subseteq>"} || @{keyword "<"})
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                     |-- Parse.!!! Parse.class)) >> Classrel),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("default_sort",Parse.opt_target -- Parse.sort
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                         >> DefaultSort),                  (* line 92 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("type_decl",Parse.opt_target -- Parse.type_args   (* line 99 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                     -- Parse.binding -- Parse.opt_mixfix
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                     >> TypeDecl),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("type_synonym",                                   (* line 104 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          let val p = Parse.opt_target -- Parse.type_args --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      Parse.binding -- (Parse.$$$ "=" |-- Parse.!!!
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                        (Parse.typ -- Parse.opt_mixfix'))
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          in p >> TypeSynonym end),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("nonterminal",Parse.and_list1 Parse.binding
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                        >> Nonterminal),                   (* line 110 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("arities",Scan.repeat1 Parse.arity >> Arities),   (* line 115 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("judgement",Parse.const_binding >> Judgement),    (* line 122 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("consts",Scan.repeat1 Parse.const_binding
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                   >> Consts),                             (* line 126 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("syntax",opt_mode -- Scan.repeat1 Parse.const_decl
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                   >> Syntax),                             (* line 137 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("no_syntax",opt_mode -- Scan.repeat1
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      Parse.const_decl  >> Syntax),        (* line 141 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("translations",Scan.repeat1 trans_line
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                         >> Translations),                 (* line 162 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("no_translations",Scan.repeat1 trans_line
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                         >> NoTranslations),               (* line 166 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("axioms",Scan.repeat1 Parse_Spec.spec >> Axioms), (* line 173 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("defs",                                           (* line 186 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          let val opt_unchecked_overloaded =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder               Scan.optional (@{keyword "("} |-- Parse.!!!
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                (((@{keyword "unchecked"} >> K true) --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                 Scan.optional (@{keyword "overloaded"} >> K true) false ||
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                 @{keyword "overloaded"} >> K (false, true)) --|
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                 @{keyword ")"})) (false, false);
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          in opt_unchecked_overloaded --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder              Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                             >> (fn ((x, y), z) => ((x, z), y)))
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder            >> Defs end),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("definition",Parse.opt_target -- Parse_Spec.constdef
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       >> Definition),                     (* line 195 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("abbreviation",Parse.opt_target --                (* line 199 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                         (opt_mode -- (Scan.option
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                          Parse_Spec.constdecl --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                          Parse.prop)) >> Abbreviation),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("type_notation",Parse.opt_target --               (* line 204 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                          (opt_mode -- Parse.and_list1
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                           (Parse.type_const -- Parse.mixfix))
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                         >> TypeNotation),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("no_type_notation",Parse.opt_target --            (* line 210 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                            (opt_mode -- Parse.and_list1
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                             (Parse.type_const -- Parse.mixfix))
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                            >> NoTypeNotation),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("notation",Parse.opt_target --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                    (opt_mode -- Parse.and_list1
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                     (Parse.const -- Parse_Spec.locale_mixfix))
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                     >> Notation),                         (* line 216 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("no_notation",Parse.opt_target --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                    (opt_mode -- Parse.and_list1
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                     (Parse.const -- Parse_Spec.locale_mixfix))
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                     >> NoNotation),                       (* line 216 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("axiomatization",Scan.optional Parse.fixes [] --  (* line 231 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                          Scan.optional (Parse.where_ |--
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                           Parse.!!! (Parse.and_list1
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                            Parse_Spec.specs)) []
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                          >> Axiomatization),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("theorems",Parse.opt_target --                    (* line 244 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                    Parse_Spec.name_facts --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                    Parse.for_fixes >> Theorems),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("lemmas",Parse.opt_target --                      (* line 248 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                  Parse_Spec.name_facts --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                  Parse.for_fixes >> Lemmas),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("declare",Parse.opt_target --                     (* line 251 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                   Parse.and_list1 Parse_Spec.xthms1 --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                   Parse.for_fixes >> Declare),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("hide_class",(Parse.opt_keyword "open" >> not) -- (* line 264 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      Scan.repeat1 Parse.xname
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      >> hide "class"),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("hide_type",(Parse.opt_keyword "open" >> not) --  (* line 265 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      Scan.repeat1 Parse.xname
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      >> hide "type"),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("hide_const",(Parse.opt_keyword "open" >> not) -- (* line 266 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      Scan.repeat1 Parse.xname
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      >> hide "const"),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("hide_fact",(Parse.opt_keyword "open" >> not) --  (* line 267 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      Scan.repeat1 Parse.xname
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      >> hide "fact"),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("use",Parse.path >> Use),                         (* line 273 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("ML",Parse.ML_source >> ML),                      (* line 280 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("ML_prf",Parse.ML_source >> ML_prf),              (* line 287 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("ML_val",Parse.ML_source >> ML_val),              (* line 293 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("ML_command",Parse.ML_source >> ML_command),      (* line 297 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("setup",Parse.ML_source >> Setup),                (* line 301 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("local_setup",Parse.opt_target --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       Parse.ML_source >> LocalSetup),     (* line 305 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("attribute_setup",Parse.position Parse.name --    (* line 309 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                           Parse.!!! (@{keyword "="} |--
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                           Parse.ML_source -- Scan.optional
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                           Parse.text "") >> AttributeSetup),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("method_setup",Parse.position Parse.name --       (* line 315 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                           Parse.!!! (@{keyword "="} |--
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                           Parse.ML_source -- Scan.optional
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                           Parse.text "") >> MethodSetup),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("declaration",Parse.opt_target --                 (* line 321 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       Parse.opt_keyword "pervasive" --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       Parse.ML_source >> Declaration),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("syntax_declaration",Parse.opt_target --          (* line 326 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       Parse.opt_keyword "pervasive" --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       Parse.ML_source >> SyntaxDeclaration),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("simproc_setup",Parse.opt_target --               (* line 331 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       Parse.position Parse.name --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       (@{keyword "("} |-- Parse.enum1 "|"
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                        Parse.term --| @{keyword ")"} --|
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                        @{keyword "="}) -- Parse.ML_source
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       -- Scan.optional (@{keyword "identifier"}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       |-- Scan.repeat1 Parse.xname) []
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       >> SimprocSetup),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("parse_ast_translation",trfun >>
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          ParseAstTranslation),                            (* line 343 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("parse_translation",trfun >> ParseTranslation),   (* line 348 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("print_translation",trfun >> PrintTranslation),   (* line 353 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("typed_print_translation", trfun >>
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          TypedPrintTranslation),                          (* line 358 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("print_ast_translation", trfun >>
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          PrintAstTranslation),                            (* line 364 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("oracle", Parse.position Parse.name --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder           (@{keyword "="} |-- Parse.ML_source) >> Oracle),(* line 371 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("bundle", Parse.opt_target -- (Parse.binding      (* line 379 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          --| @{keyword "="}) -- Parse_Spec.xthms1 --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          Parse.for_fixes >> Bundle),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("include", Scan.repeat1 (Parse.position
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                     Parse.xname) >> Include),             (* line 384 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("including", Scan.repeat1 (Parse.position
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       Parse.xname) >> Including),         (* line 390 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("print_bundles", Scan.succeed PrintBundles),      (* line 396 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("sublocale", Parse.position Parse.xname --|       (* line 434 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      (@{keyword "\<subseteq>"} ||
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       @{keyword "<"}) --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       parse_interpretation_arguments false
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder              -- proof
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                      >> Sublocale),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        ("interpretation",                                 (* line 442 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder         parse_interpretation_arguments true
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder         -- proof >> Interpretation),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("interpret",                                      (* line 449 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder         parse_interpretation_arguments true
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          >> Interpret),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("subclass",                                       (* line 471 *)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder     Parse.class -- proof >> Subclass),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    ("instance",Scan.option (Parse.class --            (* line 481 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder         (((@{keyword "\<subseteq>"} || @{keyword "<"})
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          |-- Parse.!!! Parse.class) >> InstanceSubset
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder         || Parse.multi_arity >> InstanceArity))
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder         -- proof >> Instance),
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder        ("theorem", parse_theorem -- proof >> Theorem),    (* line 525 *)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder        ("lemma", parse_theorem -- proof >> Lemma),        (* line 526 *)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder        ("corollary", parse_theorem -- proof >> Corollary),(* line 527 *)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    ("schematic_theorem", parse_theorem -- proof       (* line 528 *)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                               >> SchematicTheorem),
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    ("schematic_lemma", parse_theorem -- proof         (* line 529 *)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                             >> SchematicLemma),
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder        ("schematic_corollary", parse_theorem -- proof     (* line 530 *)
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder                             >> SchematicCorollary),
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder    (* line 313 HOL/Tools/Datatype/primrec.ML *)
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder        ("primrec", Parse.opt_target -- Parse.fixes --
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder                    Parse_Spec.where_alt_specs >> Primrec),
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder    (* line 795 HOL/Tools/Datatype/datatype.ML *)
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder    ("datatype",Parse.and_list1 Datatype.spec_cmd
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder                    >> Datatype),
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder        (* line 646 HOL/Tools/Datatype/rep_datatype.ML *)
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder        ("rep_datatype",Scan.repeat1 Parse.term
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder                        >> RepDatatype),
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder        (* line 173 HOL/Tools/Function/fun.ML *)
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder        ("fun",Function_Common.function_parser
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder                Function_Fun.fun_config
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder               >> Fun),
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder        (* line 285 HOL/Tools/Function/partial_function.ML *)
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder        ("partial_function",((@{keyword "("} |-- Parse.xname --|
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder         @{keyword ")"}) -- (Parse.fixes -- (Parse.where_ |--
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder         Parse_Spec.spec))) >> PartialFunction),
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder    (* line 284 HOL/Tools/Function/function.ML *)
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder        ("function",Function_Common.function_parser
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder                     Function_Common.default_config
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder                    -- proof
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder                    >> Function),
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder        (* line 290 HOL/Tools/Function/function.ML *)
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder        ("termination",Scan.option Parse.term -- proof
dfe355b50888d0dea1c12713288b652741844080Jonathan von Schroeder                       >> Termination)]);
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    fun unparse_cmd s = Parse.group (fn () => s)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder         (fn toks =>
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder           case toks of
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder            t::toks' =>
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder             if Token.is_command t andalso Token.content_of t = s then
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder              let val (cmd,toks'') = take_suffix Token.is_command toks'
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder              in (t::cmd |> List.map Token.unparse
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                         |> space_implode " ",toks'') end
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder             else Scan.fail ()
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder            |[] => Scan.fail ());
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    val diagnostic_commands = ["pretty_setmargin","help","print_commands",
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder         "print_configs","print_context","print_theory","print_syntax",
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder         "print_abbrevs","print_theorems","print_locales","print_classes",
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder         "print_locale","print_interps","print_dependencies",
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder         "print_attributes","print_simpset","print_rules","print_trans_rules",
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder         "print_methods","print_antiquotations","thy_deps","locale_deps",
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder         "class_deps","thm_deps","print_binds","print_facts","print_cases",
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder         "print_statement","thm","prf","full_prf","prop","term","typ",
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder         "print_codesetup","unused_thms"];
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    val toplevel_commands = ["cd","pwd","use_thy","remove_thy",
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder         "kill_thy","display_drafts","print_drafts","pr","disable_pr",
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder         "enable_pr","commit","quit","exit","welcome","init_toplevel",
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder         "linear_undo","undo","undos_proof","cannot_undo","kill",
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder         "realizers","realizability","extract_type","extract"];
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder    val simple_thy_body = simple_thy_body' ||
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder             first' (List.map (fn s => unparse_cmd s >>
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder              (Misc o DiagnosticCommand)) diagnostic_commands) ||
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder             first' (List.map (fn s => unparse_cmd s >>
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder              (Misc o TopLevelCommand)) diagnostic_commands);
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    (* Isabelle/Isar/isar_syn.ML line 415 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        val locale_val =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          Parse_Spec.locale_expression false --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          Scan.optional (@{keyword "+"} |-- Parse.!!!
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          (Scan.repeat1 Parse_Spec.context_element)) [] ||
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder        fun rec_thy_body toks = first' [
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    (Parse.command_name "context" |--                  (* line 405 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder         ((Parse.position Parse.xname >> ContextNamed) ||
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          (Scan.optional Parse_Spec.includes [] --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder           Scan.repeat Parse_Spec.context_element
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder           >> ContextHead))
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder         --| Parse.begin
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder         -- Scan.repeat (simple_thy_body || rec_thy_body)
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder         --| Parse.command_name "end"
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder         >> Context),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder         (Parse.command_name "locale" |--                  (* line 421 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          Parse.binding --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          Scan.optional (@{keyword "="} |--
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          Parse.!!! locale_val) (([], []), []) --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          ((Parse.begin |-- Scan.repeat
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder            (simple_thy_body || rec_thy_body)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder            --| Parse.command_name "end") ||
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder           Scan.succeed []) >> Locale),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          (* line 464 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          (let val class_val = (* Pure/Isar/isar_syn.ML line 458 *)
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                Parse_Spec.class_expression -- Scan.optional (@{keyword "+"}
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
0f62c81f3b90f151d8b5adde2f039948e2f0dc16Jonathan von Schroeder                Scan.repeat1 Parse_Spec.context_element >> pair []
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder              val p = Parse.binding -- Scan.optional (@{keyword "="}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                       |-- class_val) ([], [])
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          in Parse.command_name "class" |-- p --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder             ((Parse.begin |-- Scan.repeat
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder               (simple_thy_body || rec_thy_body)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder              --| Parse.command_name "end") ||
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder              Scan.succeed []) >> Class end),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          ((Parse.command_name "instantiation" |--         (* line 475 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder           Parse.multi_arity -- (Parse.begin |--
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder           Scan.repeat (simple_thy_body ||
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                        rec_thy_body)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder           --| Parse.command_name "end")) >> Instantiation),
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          (let val p = Scan.repeat1 (Parse.name --|        (* line 493 *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                (@{keyword "\<equiv>"} || @{keyword "=="}) --
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                Parse.term -- Scan.optional (@{keyword "("} |--
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                (@{keyword "unchecked"} >> K false) --|
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                @{keyword ")"}) true >> Parse.triple1)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder           in Parse.command_name "overloading" |-- p
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder              -- (Parse.begin |-- Scan.repeat
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                   (simple_thy_body || rec_thy_body) --|
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                  Parse.command_name "end")
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder              >> Overloading end)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder          ] toks;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    val thy_body = simple_thy_body || rec_thy_body;
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    (* taken from Pure/Thy/thy_load.ML *)
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder        fun read init state toks =
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder             let val master_dir = Thy_Load.get_master_path ()
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                 val spans = (*map (resolve_files master_dir)*)
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                                 (Thy_Syntax.parse_spans toks)
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                 val elements = Thy_Syntax.parse_elements spans
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                 (* fun excursion *)
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                 val immediate = not (Goal.future_enabled ())
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                 fun proof_result (tr, trs) (st, _) =
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                      let
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                        val (result, st') = Toplevel.proof_result immediate
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                                             (tr, trs) st
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                        val pos' = Toplevel.pos_of (List.last (tr :: trs))
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                      in (result, (st', pos')) end
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                 fun element_result elem x =
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                      fold_map proof_result
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                        (Outer_Syntax.read_element (#2
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                         (Outer_Syntax.get_syntax ())) init elem) x
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                val (results, (end_state, end_pos)) = fold_map element_result
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                     elements (state, Position.none)
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder             in end_state end;
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    fun init_thy (toks,header) =
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder            let val t = read (K
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                (let val {name = (name, _), imports, uses, ...} = header
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder             val _ = Thy_Header.define_keywords header
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                     val _ = Present.init_theory name
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                     val master_dir = Thy_Load.get_master_path ()
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder             val parents = List.map (Thy_Info.get_theory o #1) imports
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder             in Thy_Load.begin_theory master_dir header parents
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                 |> Present.begin_theory 0 master_dir uses end))
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder            in (t Toplevel.toplevel toks,t) end;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederend;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersignature Parser =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroedersig
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        val scan      : string -> Token.T list;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    val dbg       : Token.T list -> (Token.kind * string) list
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    datatype thy = Thy of {header:string option,
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                               args:(Token.T list * Thy_Header.header),
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                               body:(Token.T list * ParserHelper.thy_body)
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                                    list};
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    val thy : Token.T list -> thy
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    val parse_typ : theory -> (string * Position.T) option -> string -> typ
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    val pretty_tokens : unit -> unit
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederend;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederstructure Parser : Parser =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederstruct
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    open ParserHelper
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        datatype thy = Thy of {header:string option,
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                               args:(Token.T list * Thy_Header.header),
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                               body:(Token.T list * thy_body) list};
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        (* scan isabelle source transforming it into a sequence of commands *)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder        fun scan s =   File.read (Path.explode s)
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                    |> Source.of_string |> Symbol.source
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                    |> Token.source {do_recover = SOME false}
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                        Keyword.get_lexicons Position.start
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                    |> Token.source_proper |> Source.exhaust;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    val dbg = List.map (fn t => (Token.kind_of t,Token.content_of t));
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    val thy = Scan.catch (Scan.option cmd_header -- cmd_theory
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                  -- Scan.repeat thy_body
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                  --| Parse.command_name "end"
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                  #> (fn (((h,a),b),_) => Thy {header=h,args=a,body=b}));
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder    fun parse_typ T loc =
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder         let val ctxt = Named_Target.context_cmd (the_default
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder                         ("-", Position.none) loc) T
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroeder         in Syntax.parse_typ ctxt end;
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder    fun pretty_tokens () =   (Token.unparse #> PolyML.PrettyString)
18d5da8101a438aaf8c27d7e740f835e707fc0b8Jonathan von Schroeder                              |> K |> K |> PolyML.addPrettyPrinter;
3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818aJonathan von Schroederend;