Isabelle/export/parser.ml

	parser.ml revision 3a321bd2e5b11ccb6fc6afe3baf71bc0d73f818a
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowskisignature ParserHelper =
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowskisig
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski    type thy_body
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski    val cmd_theory : Thy_Header.header parser
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    val cmd_header : string parser
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    val thy_body : thy_body parser
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowskiend;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichstructure ParserHelper : ParserHelper =
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichstruct
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich    type opt_target = (xstring * Position.T) option;
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski    datatype misc_body = Chapter of opt_target * string
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich                            |Section of opt_target * string
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski                            |Subsection of opt_target * string
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich                            |Subsubsection of opt_target * string
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich                            |Text of opt_target * string
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                            |TextRaw of opt_target * string
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                            |Sect of string
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                            |Subsect of string
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                            |Subsubsect of string
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski                            |Txt of string
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski                            |TxtRaw of string;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski    type ml_text = string * Position.T;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski    (* isar-ref.pdf page 78 *)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski    datatype context_head = ContextNamed of xstring * Position.T
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski                               |ContextHead  of ((xstring * Position.T) list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski                                                * Element.context list);
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski    datatype instance_type = InstanceArity of string list * string list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski                                                 *string
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski                                |InstanceSubset of string;
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski    datatype thy_body =
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski         Classes of (binding * string list) list
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder        |Classrel of (string * string) list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski        |DefaultSort of opt_target * string
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski        |TypeDecl of ((opt_target * string list) * binding) * mixfix
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski        |TypeSynonym of ((opt_target * string list) * binding) *
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski                        (string * mixfix)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski        |Nonterminal of binding list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski        |Arities of (string * string list * string) list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski        |Judgement of (binding * string * mixfix)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski    |Consts of (binding * string * mixfix) list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski    |Syntax of (string * bool) * (string * string * mixfix) list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski        |NoSyntax of (string * bool) * (string * string * mixfix) list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski        |Translations of (xstring * string) Syntax.trrule list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski        |NoTranslations of (xstring * string) Syntax.trrule list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |Axioms of (Attrib.binding * string) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |Defs of (bool * bool) * ((binding * string) * Args.src list) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |Definition of opt_target * ((binding * string option * mixfix) option
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                       * (Attrib.binding * string))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |Abbreviation of opt_target * ((string * bool) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                          ((binding * string option * mixfix) option * string))
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |TypeNotation of opt_target * ((string * bool) * (string * mixfix) list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |NoTypeNotation of opt_target * ((string * bool) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                                         (string * mixfix) list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |Notation of opt_target * ((string * bool) * (string * mixfix) list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |NoNotation of opt_target * ((string * bool) * (string * mixfix) list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |Axiomatization of (binding * string option * mixfix) list *
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski                           (Attrib.binding * string list) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |Theorems of (opt_target * (Attrib.binding *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                      (Facts.ref * Args.src list) list) list) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                     (binding * string option * mixfix) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |Lemmas of (opt_target * (Attrib.binding *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                      (Facts.ref * Args.src list) list) list) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                     (binding * string option * mixfix) list
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski    |Declare of (opt_target * (Facts.ref * Args.src list) list list) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                    (binding * string option * mixfix) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |Hide of string * (bool * xstring list)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |Use of string
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |ML of ml_text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |ML_prf of ml_text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |ML_val of ml_text
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski        |ML_command of ml_text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |Setup of ml_text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |LocalSetup of opt_target * ml_text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |AttributeSetup of (bstring * Position.T) * (ml_text * string)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |MethodSetup of (bstring * Position.T) * (ml_text * string)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |Declaration of (opt_target * bool) * ml_text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |SyntaxDeclaration of (opt_target * bool) * ml_text
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |SimprocSetup of (((opt_target * (bstring * Position.T)) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                           string list) * ml_text) * xstring list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |ParseAstTranslation of bool * (string * Position.T)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |ParseTranslation of bool * (string * Position.T)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |PrintTranslation of bool * (string * Position.T)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |TypedPrintTranslation of bool * (string * Position.T)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |PrintAstTranslation of bool * (string * Position.T)
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich    |Oracle of (bstring * Position.T) * ml_text
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich    |Bundle of ((opt_target * binding) * (Facts.ref * Args.src list) list) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                    (binding * string option * mixfix) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |Include of (xstring * Position.T) list
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    |Including of (xstring * Position.T) list
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    |PrintBundles
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    |Context of context_head * thy_body list
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    |Locale of (binding * (Expression.expression * Element.context list))
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke                   * thy_body list
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke    |Sublocale of (xstring * Position.T) * (Expression.expression *
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                       (Attrib.binding * string) list)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    |Interpretation of Expression.expression *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                           (Attrib.binding * string) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |Interpret of Expression.expression *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                      (Attrib.binding * string) list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |Class of (binding * (string list * Element.context list)) *
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                  thy_body list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |Subclass of string
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |Instantiation of (string list * string list * string) * thy_body list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |Instance of (string * instance_type) option
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    |Overloading of (bstring * string * bool) list * thy_body list
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        |Misc of misc_body;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    val hide = curry Hide;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(* Common Functions *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    (* taken from Pure/Isar/parse.ML *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    fun RESET_VALUE atom =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski          Scan.ahead (Scan.one (K true)) -- atom >>
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski           (fn (arg, x) => (Token.assign NONE arg; x));
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        fun unparse_kind k =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski            Parse.group (fn () => Token.str_of_kind k)
a8ce558d09f304be325dc89458c9504d3ff7fe80Till Mossakowski             (RESET_VALUE (Scan.one (Token.is_kind k) >> Token.unparse));
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        val unparse_verbatim = unparse_kind Token.Verbatim;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(* Pure/pure_syn.ML *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    (* line 12 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        val cmd_theory = Parse.command_name "theory" |-- Thy_Header.args;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski(* Pure/Isar/isar_syn.ML *)
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski    (* line 14 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        val cmd_header = Parse.command_name "header" |-- unparse_verbatim;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    (* line 133 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    val opt_mode =
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski          (* line 129 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski          let val mode_spec = (@{keyword "output"} >> K ("", false)) ||
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski                              Parse.name -- Scan.optional
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                               (@{keyword "output"} >> K false) true;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski          in Scan.optional (@{keyword "("} |-- Parse.!!!
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski              (mode_spec --| @{keyword ")"})) Syntax.mode_default end;
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    val trans_line = (* line 157 *)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder          let val trans_pat = (* line 147 *)
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder                   Scan.optional
3e0309de8bbb1588c0f976d6ce3f1e615d17da84Christian Maeder                    (@{keyword "("} |-- Parse.!!!
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder                     (Parse.xname --| @{keyword ")"}))
d78a2b8c5a63f3e63393e5cc44a5e9b253ac459bChristian Maeder                    "logic" -- Parse.inner_syntax Parse.string
464c78620a182d2e8fbd125098045eae8788e2bdTill Mossakowski              fun trans_arrow toks = (* line 152 *)
12a1614014912501fbfc30a74242d6f3a5c97e80Till Mossakowski                  ((@{keyword "\<rightharpoonup>"} || @{keyword "=>"})
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                   >> K Syntax.Parse_Rule ||
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                  (@{keyword "\<leftharpoondown>"} || @{keyword "<="})
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                   >> K Syntax.Print_Rule ||
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                  (@{keyword "\<rightleftharpoons>"} || @{keyword "=="})
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                   >> K Syntax.Parse_Print_Rule) toks
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski      in trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski        >> (fn (left, (arr, right)) => arr (left, right)) end;
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski    val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski    fun parse_interpretation_arguments mandatory = (* line 428 *)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski      Parse.!!! (Parse_Spec.locale_expression mandatory) --
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski        Scan.optional
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski          (Parse.where_ |-- Parse.and_list1
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski               (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski    val mk_thy_body = List.map (fn (s,p) => Parse.command_name s |-- p);
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski    val simple_thy_body = Scan.first (mk_thy_body [
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski    ("chapter", Parse.opt_target -- unparse_verbatim
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski                     >> (Misc o Chapter)),                 (* line 19 *)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski    ("section", Parse.opt_target -- unparse_verbatim
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski                     >> (Misc o Section)),                 (* line 24 *)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski        ("subsection", Parse.opt_target -- unparse_verbatim
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski                        >> (Misc o Subsection)),           (* line 29 *)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski        ("subsubsection", Parse.opt_target -- unparse_verbatim
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski                           >> (Misc o Subsubsection)),     (* line 34 *)
65afd6de83b252cc393ee407bab4dd8b57b97e0bDominik Luecke        ("text", Parse.opt_target -- unparse_verbatim
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski                  >> (Misc o Text)),                       (* line 39 *)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski        ("text_raw", Parse.opt_target -- unparse_verbatim
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski                      >> (Misc o Text)),                   (* line 44 *)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski    ("sect", unparse_verbatim >> (Misc o Sect)),       (* line 49 *)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski    ("subsect", unparse_verbatim >> (Misc o Sect)),    (* line 54 *)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski        ("subsubsect", unparse_verbatim
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder                        >> (Misc o Subsubsect)),           (* line 59 *)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski    ("txt", unparse_verbatim >> (Misc o Txt)),         (* line 64 *)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski        ("txt_raw", unparse_verbatim >> (Misc o TxtRaw)),  (* line 69 *)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski    ("classes",Scan.repeat1 (Parse.binding --          (* line 79 *)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski                    Scan.optional ((@{keyword "\<subseteq>"}
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski                     || @{keyword "<"}) |-- Parse.!!!
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski                    (Parse.list1 Parse.class)) []) >> Classes),
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski        ("classrel",Parse.and_list1 (Parse.class --        (* line 85 *)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski                     ((@{keyword "\<subseteq>"} || @{keyword "<"})
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski                     |-- Parse.!!! Parse.class)) >> Classrel),
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski        ("default_sort",Parse.opt_target -- Parse.sort
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski                         >> DefaultSort),                  (* line 92 *)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski        ("type_decl",Parse.opt_target -- Parse.type_args   (* line 99 *)
c9d53cd78829e538aee56b84db508d8d944e6551Till Mossakowski                     -- Parse.binding -- Parse.opt_mixfix
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski                     >> TypeDecl),
30256573a343132354b122097b0ee1215dda1364Till Mossakowski    ("type_synonym",                                   (* line 104 *)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski          let val p = Parse.opt_target -- Parse.type_args --
30256573a343132354b122097b0ee1215dda1364Till Mossakowski                      Parse.binding -- (Parse.$$$ "=" |-- Parse.!!!
30256573a343132354b122097b0ee1215dda1364Till Mossakowski                        (Parse.typ -- Parse.opt_mixfix'))
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder          in p >> TypeSynonym end),
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder    ("nonterminal",Parse.and_list1 Parse.binding
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder                        >> Nonterminal),                   (* line 110 *)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder    ("arities",Scan.repeat1 Parse.arity >> Arities),   (* line 115 *)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski    ("judgement",Parse.const_binding >> Judgement),    (* line 122 *)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski        ("consts",Scan.repeat1 Parse.const_binding
30256573a343132354b122097b0ee1215dda1364Till Mossakowski                   >> Consts),                             (* line 126 *)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski    ("syntax",opt_mode -- Scan.repeat1 Parse.const_decl
30256573a343132354b122097b0ee1215dda1364Till Mossakowski                   >> Syntax),                             (* line 137 *)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski    ("no_syntax",opt_mode -- Scan.repeat1
30256573a343132354b122097b0ee1215dda1364Till Mossakowski                      Parse.const_decl  >> Syntax),        (* line 141 *)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski    ("translations",Scan.repeat1 trans_line
30256573a343132354b122097b0ee1215dda1364Till Mossakowski                         >> Translations),                 (* line 162 *)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski    ("no_translations",Scan.repeat1 trans_line
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder                         >> NoTranslations),               (* line 166 *)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski    ("axioms",Scan.repeat1 Parse_Spec.spec >> Axioms), (* line 173 *)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski    ("defs",                                           (* line 186 *)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski          let val opt_unchecked_overloaded =
30256573a343132354b122097b0ee1215dda1364Till Mossakowski               Scan.optional (@{keyword "("} |-- Parse.!!!
30256573a343132354b122097b0ee1215dda1364Till Mossakowski                (((@{keyword "unchecked"} >> K true) --
30256573a343132354b122097b0ee1215dda1364Till Mossakowski                 Scan.optional (@{keyword "overloaded"} >> K true) false ||
30256573a343132354b122097b0ee1215dda1364Till Mossakowski                 @{keyword "overloaded"} >> K (false, true)) --|
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                 @{keyword ")"})) (false, false);
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski          in opt_unchecked_overloaded --
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski              Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop
376b6600e1ccebd180299471f732b008a96027d4Till Mossakowski                             >> (fn ((x, y), z) => ((x, z), y)))
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski            >> Defs end),
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder    ("definition",Parse.opt_target -- Parse_Spec.constdef
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                       >> Definition),                     (* line 195 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    ("abbreviation",Parse.opt_target --                (* line 199 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                         (opt_mode -- (Scan.option
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                          Parse_Spec.constdecl --
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                          Parse.prop)) >> Abbreviation),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    ("type_notation",Parse.opt_target --               (* line 204 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                          (opt_mode -- Parse.and_list1
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                           (Parse.type_const -- Parse.mixfix))
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski                         >> TypeNotation),
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski    ("no_type_notation",Parse.opt_target --            (* line 210 *)
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski                            (opt_mode -- Parse.and_list1
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski                             (Parse.type_const -- Parse.mixfix))
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski                            >> NoTypeNotation),
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski    ("notation",Parse.opt_target --
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski                    (opt_mode -- Parse.and_list1
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski                     (Parse.const -- Parse_Spec.locale_mixfix))
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski                     >> Notation),                         (* line 216 *)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski    ("no_notation",Parse.opt_target --
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                    (opt_mode -- Parse.and_list1
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                     (Parse.const -- Parse_Spec.locale_mixfix))
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                     >> NoNotation),                       (* line 216 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    ("axiomatization",Scan.optional Parse.fixes [] --  (* line 231 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                          Scan.optional (Parse.where_ |--
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder                           Parse.!!! (Parse.and_list1
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski                            Parse_Spec.specs)) []
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                          >> Axiomatization),
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski    ("theorems",Parse.opt_target --                    (* line 244 *)
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                    Parse_Spec.name_facts --
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                    Parse.for_fixes >> Theorems),
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski        ("lemmas",Parse.opt_target --                      (* line 248 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                  Parse_Spec.name_facts --
d3f2015ae170a15e5b57d4880ded53073d725ac0Till Mossakowski                  Parse.for_fixes >> Lemmas),
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski    ("declare",Parse.opt_target --                     (* line 251 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                   Parse.and_list1 Parse_Spec.xthms1 --
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                   Parse.for_fixes >> Declare),
f2d72b2254513ef810b0951f0b13a62c2921cb4dTill Mossakowski    ("hide_class",(Parse.opt_keyword "open" >> not) -- (* line 264 *)
881ab7022a03f9a6fa697d3067d05d61844929cbChristian Maeder                      Scan.repeat1 Parse.xname
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder                      >> hide "class"),
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder    ("hide_type",(Parse.opt_keyword "open" >> not) --  (* line 265 *)
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder                      Scan.repeat1 Parse.xname
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder                      >> hide "type"),
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder    ("hide_const",(Parse.opt_keyword "open" >> not) -- (* line 266 *)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski                      Scan.repeat1 Parse.xname
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder                      >> hide "const"),
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder    ("hide_fact",(Parse.opt_keyword "open" >> not) --  (* line 267 *)
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder                      Scan.repeat1 Parse.xname
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder                      >> hide "fact"),
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder    ("use",Parse.path >> Use),                         (* line 273 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    ("ML",Parse.ML_source >> ML),                      (* line 280 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    ("ML_prf",Parse.ML_source >> ML_prf),              (* line 287 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    ("ML_val",Parse.ML_source >> ML_val),              (* line 293 *)
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder    ("ML_command",Parse.ML_source >> ML_command),      (* line 297 *)
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz    ("setup",Parse.ML_source >> Setup),                (* line 301 *)
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder    ("local_setup",Parse.opt_target --
3532dcfda4dd76997072fcda24e75c305d105233Till Mossakowski                       Parse.ML_source >> LocalSetup),     (* line 305 *)
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder    ("attribute_setup",Parse.position Parse.name --    (* line 309 *)
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder                           Parse.!!! (@{keyword "="} |--
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder                           Parse.ML_source -- Scan.optional
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder                           Parse.text "") >> AttributeSetup),
0093b49b89d814da4164d43e754509a90a00e9eeChristian Maeder    ("method_setup",Parse.position Parse.name --       (* line 315 *)
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder                           Parse.!!! (@{keyword "="} |--
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian Maeder                           Parse.ML_source -- Scan.optional
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maeder                           Parse.text "") >> MethodSetup),
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulz    ("declaration",Parse.opt_target --                 (* line 321 *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski                       Parse.opt_keyword "pervasive" --
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                       Parse.ML_source >> Declaration),
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski    ("syntax_declaration",Parse.opt_target --          (* line 326 *)
38a46398edcd7ad7d1777ae646d4cc484cce49bfTill Mossakowski                       Parse.opt_keyword "pervasive" --
5277e290ad70afdf97f359019afd8fb5816f4102Till Mossakowski                       Parse.ML_source >> SyntaxDeclaration),
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    ("simproc_setup",Parse.opt_target --               (* line 331 *)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder                       Parse.position Parse.name --
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                       (@{keyword "("} |-- Parse.enum1 "|"
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                        Parse.term --| @{keyword ")"} --|
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                        @{keyword "="}) -- Parse.ML_source
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                       -- Scan.optional (@{keyword "identifier"}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                       |-- Scan.repeat1 Parse.xname) []
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                       >> SimprocSetup),
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    ("parse_ast_translation",trfun >>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski          ParseAstTranslation),                            (* line 343 *)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder        ("parse_translation",trfun >> ParseTranslation),   (* line 348 *)
30256573a343132354b122097b0ee1215dda1364Till Mossakowski        ("print_translation",trfun >> PrintTranslation),   (* line 353 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski        ("typed_print_translation", trfun >>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski          TypedPrintTranslation),                          (* line 358 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    ("print_ast_translation", trfun >>
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski          PrintAstTranslation),                            (* line 364 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    ("oracle", Parse.position Parse.name --
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski           (@{keyword "="} |-- Parse.ML_source) >> Oracle),(* line 371 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski        ("bundle", Parse.opt_target -- (Parse.binding      (* line 379 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski          --| @{keyword "="}) -- Parse_Spec.xthms1 --
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski          Parse.for_fixes >> Bundle),
7a8592051724fa46499bde120f44cdc8db270876Till Mossakowski    ("include", Scan.repeat1 (Parse.position
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                     Parse.xname) >> Include),             (* line 384 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    ("including", Scan.repeat1 (Parse.position
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski                       Parse.xname) >> Including),         (* line 390 *)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski    ("print_bundles", Scan.succeed PrintBundles),      (* line 396 *)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder        ("sublocale", Parse.position Parse.xname --|       (* line 434 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                      (@{keyword "\<subseteq>"} ||
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder                       @{keyword "<"}) --
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                       parse_interpretation_arguments false
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu                      >> Sublocale),
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu        ("interpretation",                                 (* line 442 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski         parse_interpretation_arguments true
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski          >> Interpretation),
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    ("interpret",                                      (* line 449 *)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder         parse_interpretation_arguments true
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski          >> Interpret),
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski    ("subclass",                                       (* line 471 *)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski     Parse.class >> Subclass),
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    ("instance",Scan.option (Parse.class --            (* line 481 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski         (((@{keyword "\<subseteq>"} || @{keyword "<"})
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski          |-- Parse.!!! Parse.class) >> InstanceSubset
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski         || Parse.multi_arity >> InstanceArity))
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski         >> Instance)]);
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    (* Isabelle/Isar/isar_syn.ML line 415 *)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder        val locale_val =
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder          Parse_Spec.locale_expression false --
30256573a343132354b122097b0ee1215dda1364Till Mossakowski          Scan.optional (@{keyword "+"} |-- Parse.!!!
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder          (Scan.repeat1 Parse_Spec.context_element)) [] ||
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder          Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder        fun rec_thy_body toks = Scan.first [
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski    (Parse.command_name "context" |--                  (* line 405 *)
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski         ((Parse.position Parse.xname >> ContextNamed) ||
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski          (Scan.optional Parse_Spec.includes [] --
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski           Scan.repeat Parse_Spec.context_element
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski           >> ContextHead))
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich         --| Parse.begin
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski         -- Scan.repeat (simple_thy_body || rec_thy_body)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder         >> Context),
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski         (Parse.command_name "locale" |--                  (* line 421 *)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski          Parse.binding --
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski          Scan.optional (@{keyword "="} |--
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski          Parse.!!! locale_val) (([], []), []) --
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder          ((Parse.begin |-- Scan.repeat
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder            (simple_thy_body || rec_thy_body)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski            --| Parse.command_name "end") ||
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski           Scan.succeed []) >> Locale),
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski          (* line 464 *)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder          (let val class_val = (* Pure/Isar/isar_syn.ML line 458 *)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski                Parse_Spec.class_expression -- Scan.optional (@{keyword "="}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                 |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) []
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                 || Scan.repeat1 Parse_Spec.context_element >> pair []
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski              val p = Parse.binding -- Scan.optional (@{keyword "="}
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski                       |-- class_val) ([], [])
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski          in Parse.command_name "class" |-- p --
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski             ((Parse.begin |-- Scan.repeat
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski               (simple_thy_body || rec_thy_body)
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski              --| Parse.command_name "end") ||
91dd24480df03b2cca7c1645bb2866d7000dfdb1Till Mossakowski              Scan.succeed []) >> Class end),
30256573a343132354b122097b0ee1215dda1364Till Mossakowski          ((Parse.command_name "instantiation" |--         (* line 475 *)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder           Parse.multi_arity -- (Parse.begin |--
9c3b1fb1952bb78a1942fe612215f940fc8e5f31Till Mossakowski           Scan.repeat (simple_thy_body ||
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder                        rec_thy_body)
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder           --| Parse.command_name "end")) >> Instantiation),
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder          (let val p = Scan.repeat1 (Parse.name --|        (* line 493 *)
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu                (@{keyword "\<equiv>"} || @{keyword "=="}) --
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu                Parse.term -- Scan.optional (@{keyword "("} |--
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski                (@{keyword "unchecked"} >> K false) --|
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich                @{keyword ")"}) true >> Parse.triple1)
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski           in Parse.command_name "overloading" |-- p
2642069f1e829a4eb80dd1d235482ce2a86dc57eKlaus Luettich              -- (Parse.begin |-- Scan.repeat
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski                   (simple_thy_body || rec_thy_body) --|
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski                  Parse.command_name "end")
89118fd658073a87eddf4ead4bb63c6adb30550dTill Mossakowski              >> Overloading end)
8d576513b8c89016a3d678378ed75cac0e2e1aefChristian Maeder          ] toks;
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettich    val thy_body = simple_thy_body || rec_thy_body;
e7eefd526faedd63acb8f91de5793368cfe67655Klaus Luettichend;
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu
533d6033bec94a46d13b73cafe40953f699757c7Christian Maedersignature Parser =
533d6033bec94a46d13b73cafe40953f699757c7Christian Maedersig
533d6033bec94a46d13b73cafe40953f699757c7Christian Maeder        val scan      : string -> Token.T list;
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu    val dbg       : Token.T list -> (Token.kind * string) list
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder    datatype thy = Thy of {header:string option,
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu                               args:Thy_Header.header,
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder                               body:ParserHelper.thy_body list};
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maeder    val thy : Token.T list -> thy
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu    val parse_typ : theory -> (string * Position.T) option -> string -> typ
6eb84b5a2295c866c59905963b9342bc120b75ebEwaryst Schulzend;
9db773679fcc0a65c04b99f5699d3db382b6be7aEwaryst Schulz
2a5598bba75f2fbaa7851a9be2f8f0a1fce19cb6Ewaryst Schulzstructure Parser : Parser =
749b7d8ea5a481831375f49ae50239dd8e3d2d12Christian Maederstruct
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maeder    open ParserHelper
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maeder        datatype thy = Thy of {header:string option,
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maeder                               args:Thy_Header.header,
4317329b15d986d363c78acf8e4b330f33cccf9dChristian Maeder                               body:thy_body list};
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu        (* scan isabelle source transforming it into a sequence of commands *)
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu        fun scan s =   File.read (Path.explode s)
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu                    |> Source.of_string |> Symbol.source
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu                    |> Token.source {do_recover = SOME false}
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder                        Keyword.get_lexicons Position.start
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu                    |> Token.source_proper |> Source.exhaust;
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu    val dbg = List.map (fn t => (Token.kind_of t,Token.content_of t));
de55550f7d117195f127481d18ec2d5e8d2317ffMihai Codescu    val thy = Scan.catch (Scan.option cmd_header -- cmd_theory
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder                  -- Scan.repeat thy_body
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder                  --| Parse.command_name "end"
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu                  #> (fn (((h,a),b),_) => Thy {header=h,args=a,body=b}));
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu    fun parse_typ T loc =
543ded2ae6a6e13f6cd2c22f9f0921e8c452cba0Christian Maeder         let val ctxt = Named_Target.context_cmd (the_default
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian Maeder                         ("-", Position.none) loc) T
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian Maeder         in Syntax.parse_typ ctxt end;
3fdf6c17476458d1458d5ae2c085efd2634ba7d9Christian Maederend;
c57bde4abc9029546fa396c4eccacf969e126b96Mihai Codescu