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