# HG changeset patch # User wenzelm # Date 1013542107 -3600 # Node ID a70df1e5bf1023a8ca3cb9eadef13f0578a36aac # Parent bda60442bf02a98a54b2ec67a4635d5da7d3c532 got rid of explicit marginal comments (now stripped earlier from input); diff -r bda60442bf02 -r a70df1e5bf10 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/HOL/Tools/datatype_package.ML Tue Feb 12 20:28:27 2002 +0100 @@ -858,12 +858,13 @@ val datatype_decl = Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix -- - (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix --| P.marg_comment)); + (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix)); fun mk_datatype args = let val names = map (fn ((((None, _), t), _), _) => t | ((((Some t, _), _), _), _) => t) args; - val specs = map (fn ((((_, vs), t), mx), cons) => (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args; + val specs = map (fn ((((_, vs), t), mx), cons) => + (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args; in #1 o add_datatype false names specs end; val datatypeP = diff -r bda60442bf02 -r a70df1e5bf10 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/HOL/Tools/inductive_package.ML Tue Feb 12 20:28:27 2002 +0100 @@ -44,10 +44,8 @@ val inductive_forall_name: string val inductive_forall_def: thm val rulify: thm -> thm - val inductive_cases: (((bstring * Args.src list) * string list) * Comment.text) list - -> theory -> theory - val inductive_cases_i: (((bstring * theory attribute list) * term list) * Comment.text) list - -> theory -> theory + val inductive_cases: ((bstring * Args.src list) * string list) list -> theory -> theory + val inductive_cases_i: ((bstring * theory attribute list) * term list) list -> theory -> theory val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list -> ((bstring * term) * theory attribute list) list -> thm list -> theory -> theory * {defs: thm list, elims: thm list, raw_induct: thm, induct: thm, @@ -587,8 +585,8 @@ val cert_prop = Thm.cterm_of (Theory.sign_of thy) o prep_prop (ProofContext.init thy); val mk_cases = smart_mk_cases thy (Simplifier.simpset_of thy) o cert_prop; - val facts = args |> map (fn (((a, atts), props), comment) => - (((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props), comment)); + val facts = args |> map (fn ((a, atts), props) => + ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props)); in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end; val inductive_cases = gen_inductive_cases Attrib.global_attribute ProofContext.read_prop; @@ -874,10 +872,10 @@ #1 o add_inductive true coind sets (map P.triple_swap intrs) monos; fun ind_decl coind = - (Scan.repeat1 P.term --| P.marg_comment) -- + Scan.repeat1 P.term -- (P.$$$ "intros" |-- - P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) -- - Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] + P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) -- + Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] >> (Toplevel.theory o mk_ind coind); val inductiveP = @@ -888,7 +886,7 @@ val ind_cases = - P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop -- P.marg_comment) + P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop) >> (Toplevel.theory o inductive_cases); val inductive_casesP = diff -r bda60442bf02 -r a70df1e5bf10 src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/HOL/Tools/primrec_package.ML Tue Feb 12 20:28:27 2002 +0100 @@ -291,7 +291,7 @@ val primrec_decl = Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" -- - Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment); + Scan.repeat1 (P.opt_thm_name ":" -- P.prop); val primrecP = OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl diff -r bda60442bf02 -r a70df1e5bf10 src/HOL/Tools/recdef_package.ML --- a/src/HOL/Tools/recdef_package.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/HOL/Tools/recdef_package.ML Tue Feb 12 20:28:27 2002 +0100 @@ -310,8 +310,8 @@ error ("No termination condition #" ^ string_of_int i ^ " in recdef definition of " ^ quote name); in - thy |> IsarThy.theorem_i Drule.internalK - (((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))), Comment.none) int + thy + |> IsarThy.theorem_i Drule.internalK ((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))) int end; val recdef_tc = gen_recdef_tc Attrib.global_attribute Sign.intern_const; @@ -340,8 +340,7 @@ val recdef_decl = Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true -- - P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment) - -- Scan.option hints + P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop) -- Scan.option hints >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src); val recdefP = @@ -360,8 +359,7 @@ val recdef_tc_decl = - P.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") - --| P.marg_comment; + P.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")"); fun mk_recdef_tc ((thm_name, name), i) = recdef_tc thm_name name i; diff -r bda60442bf02 -r a70df1e5bf10 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/HOL/Tools/record_package.ML Tue Feb 12 20:28:27 2002 +0100 @@ -1086,8 +1086,8 @@ local structure P = OuterParse and K = OuterSyntax.Keyword in val record_decl = - P.type_args -- P.name -- (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") - -- Scan.repeat1 (P.const --| P.marg_comment)); + P.type_args -- P.name -- + (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const); val recordP = OuterSyntax.command "record" "define extensible record" K.thy_decl diff -r bda60442bf02 -r a70df1e5bf10 src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/HOL/Tools/typedef_package.ML Tue Feb 12 20:28:27 2002 +0100 @@ -22,11 +22,9 @@ {type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm, Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm, Rep_induct: thm, Abs_induct: thm} - val typedef_proof: - (string * (bstring * string list * mixfix) * string * (string * string) option) * Comment.text + val typedef_proof: string * (bstring * string list * mixfix) * string * (string * string) option -> bool -> theory -> ProofHistory.T - val typedef_proof_i: - (string * (bstring * string list * mixfix) * term * (string * string) option) * Comment.text + val typedef_proof_i: string * (bstring * string list * mixfix) * term * (string * string) option -> bool -> theory -> ProofHistory.T end; @@ -241,15 +239,12 @@ (* typedef_proof interface *) -fun gen_typedef_proof prep_term ((name, typ, set, opt_morphs), comment) int thy = +fun gen_typedef_proof prep_term (name, typ, set, opt_morphs) int thy = let val (_, goal, goal_pat, att_result) = prepare_typedef prep_term true name typ set opt_morphs thy; val att = #1 o att_result; - in - thy - |> IsarThy.theorem_i Drule.internalK ((("", [att]), (goal, ([goal_pat], []))), comment) int - end; + in thy |> IsarThy.theorem_i Drule.internalK (("", [att]), (goal, ([goal_pat], []))) int end; val typedef_proof = gen_typedef_proof read_term; val typedef_proof_i = gen_typedef_proof cert_term; @@ -262,18 +257,17 @@ val typedeclP = OuterSyntax.command "typedecl" "type declaration (HOL)" K.thy_decl - (P.type_args -- P.name -- P.opt_infix --| P.marg_comment >> (fn ((vs, t), mx) => + (P.type_args -- P.name -- P.opt_infix >> (fn ((vs, t), mx) => Toplevel.theory (add_typedecls [(t, vs, mx)]))); val typedef_proof_decl = Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- - Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name)) -- - P.marg_comment; + Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name)); -fun mk_typedef_proof (((((opt_name, (vs, t)), mx), A), morphs), comment) = - typedef_proof ((if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A, morphs), comment); +fun mk_typedef_proof ((((opt_name, (vs, t)), mx), A), morphs) = + typedef_proof (if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A, morphs); val typedefP = OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal @@ -285,5 +279,4 @@ end; - end; diff -r bda60442bf02 -r a70df1e5bf10 src/HOLCF/cont_consts.ML --- a/src/HOLCF/cont_consts.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/HOLCF/cont_consts.ML Tue Feb 12 20:28:27 2002 +0100 @@ -110,7 +110,7 @@ thy |> consts (map fst args) |> defs (false, map (fn ((c, _, mx), s) => - (((Thm.def_name (Syntax.const_name c mx), s), []), Comment.none)) args); + ((Thm.def_name (Syntax.const_name c mx), s), [])) args); fun add_constdefs args = gen_add_constdefs add_consts IsarThy.add_defs args; fun add_constdefs_i args = gen_add_constdefs add_consts_i IsarThy.add_defs_i args; @@ -122,12 +122,11 @@ val constsP = OuterSyntax.command "consts" "declare constants (HOLCF)" K.thy_decl - (Scan.repeat1 (P.const --| P.marg_comment) >> (Toplevel.theory o add_consts)); + (Scan.repeat1 P.const >> (Toplevel.theory o add_consts)); val constdefsP = OuterSyntax.command "constdefs" "declare and define constants (HOLCF)" K.thy_decl - (Scan.repeat1 ((P.const --| P.marg_comment) -- (P.term --| P.marg_comment)) - >> (Toplevel.theory o add_constdefs)); + (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o add_constdefs)); val _ = OuterSyntax.add_parsers [constsP, constdefsP]; diff -r bda60442bf02 -r a70df1e5bf10 src/HOLCF/domain/extender.ML --- a/src/HOLCF/domain/extender.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/HOLCF/domain/extender.ML Tue Feb 12 20:28:27 2002 +0100 @@ -124,7 +124,7 @@ P.name -- (P.$$$ "::" |-- P.typ) --| P.$$$ ")" >> P.triple1; val cons_decl = - P.name -- Scan.repeat dest_decl -- P.opt_mixfix --| P.marg_comment + P.name -- Scan.repeat dest_decl -- P.opt_mixfix >> (fn ((c, ds), mx) => (c, mx, ds)); val domain_decl = (P.type_args -- P.name >> Library.swap) -- (P.$$$ "=" |-- P.enum1 "|" cons_decl); diff -r bda60442bf02 -r a70df1e5bf10 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Tue Feb 12 20:28:27 2002 +0100 @@ -29,11 +29,10 @@ val undo_theory: Toplevel.transition -> Toplevel.transition val undo: Toplevel.transition -> Toplevel.transition val kill: Toplevel.transition -> Toplevel.transition - val back: bool * Comment.text -> Toplevel.transition -> Toplevel.transition - val use: string * Comment.text -> Toplevel.transition -> Toplevel.transition - val use_mltext_theory: string * Comment.text -> Toplevel.transition -> Toplevel.transition - val use_mltext: bool -> string * Comment.text -> Toplevel.transition -> Toplevel.transition - val use_setup: string * Comment.text -> theory -> theory + val back: bool -> Toplevel.transition -> Toplevel.transition + val use: string -> Toplevel.transition -> Toplevel.transition + val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition + val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition val use_commit: Toplevel.transition -> Toplevel.transition val cd: string -> Toplevel.transition -> Toplevel.transition val pwd: Toplevel.transition -> Toplevel.transition @@ -47,7 +46,7 @@ val print_syntax: Toplevel.transition -> Toplevel.transition val print_theorems: Toplevel.transition -> Toplevel.transition val print_locales: Toplevel.transition -> Toplevel.transition - val print_locale: Locale.expr * (Args.src Locale.element * Comment.text) list + val print_locale: Locale.expr * Args.src Locale.element list -> Toplevel.transition -> Toplevel.transition val print_attributes: Toplevel.transition -> Toplevel.transition val print_rules: Toplevel.transition -> Toplevel.transition @@ -60,16 +59,13 @@ val print_binds: Toplevel.transition -> Toplevel.transition val print_lthms: Toplevel.transition -> Toplevel.transition val print_cases: Toplevel.transition -> Toplevel.transition - val print_thms: (string list * (string * Args.src list) list) * Comment.text + val print_thms: string list * (string * Args.src list) list -> Toplevel.transition -> Toplevel.transition - val print_prfs: bool -> (string list * (string * Args.src list) list option) * Comment.text + val print_prfs: bool -> string list * (string * Args.src list) list option -> Toplevel.transition -> Toplevel.transition - val print_prop: (string list * string) * Comment.text - -> Toplevel.transition -> Toplevel.transition - val print_term: (string list * string) * Comment.text - -> Toplevel.transition -> Toplevel.transition - val print_type: (string list * string) * Comment.text - -> Toplevel.transition -> Toplevel.transition + val print_prop: (string list * string) -> Toplevel.transition -> Toplevel.transition + val print_term: (string list * string) -> Toplevel.transition -> Toplevel.transition + val print_type: (string list * string) -> Toplevel.transition -> Toplevel.transition end; structure IsarCmd: ISAR_CMD = @@ -135,26 +131,23 @@ val undo = Toplevel.kill o undo_theory o undos_proof 1; val kill = Toplevel.kill o kill_proof; - -val back = Toplevel.proof o ProofHistory.back o Comment.ignore; +val back = Toplevel.proof o ProofHistory.back; (* use ML text *) -fun use (name, comment_ignore) = Toplevel.keep (fn state => +fun use name = Toplevel.keep (fn state => Context.setmp (try Toplevel.theory_of state) ThyInfo.use name); (*passes changes of theory context*) -val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory o Comment.ignore; +val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory; (*ignore result theory context*) -fun use_mltext v (txt, comment_ignore) = Toplevel.keep' (fn verb => fn state => +fun use_mltext v txt = Toplevel.keep' (fn verb => fn state => (Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state))); -val use_setup = Context.use_setup o Comment.ignore; - (*Note: commit is dynamically bound*) -val use_commit = use_mltext false ("commit();", Comment.none); +val use_commit = use_mltext false "commit();"; (* current working directory *) @@ -196,8 +189,7 @@ fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state => let val thy = Toplevel.theory_of state in - Locale.print_locale thy import - (map (Locale.attribute (Attrib.local_attribute thy) o Comment.ignore) body) + Locale.print_locale thy import (map (Locale.attribute (Attrib.local_attribute thy)) body) end); val print_attributes = Toplevel.unknown_theory o @@ -291,11 +283,10 @@ fun print_item string_of (x, y) = Toplevel.keep (fn state => writeln (string_of (Toplevel.enter_forward_proof state) x y)); -val print_thms = print_item string_of_thms o Comment.ignore; -fun print_prfs full = print_item (string_of_prfs full) o Comment.ignore; -val print_prop = print_item string_of_prop o Comment.ignore; -val print_term = print_item string_of_term o Comment.ignore; -val print_type = print_item string_of_type o Comment.ignore; - +val print_thms = print_item string_of_thms; +fun print_prfs full = print_item (string_of_prfs full); +val print_prop = print_item string_of_prop; +val print_term = print_item string_of_term; +val print_type = print_item string_of_type; end; diff -r bda60442bf02 -r a70df1e5bf10 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/Pure/Isar/isar_syn.ML Tue Feb 12 20:28:27 2002 +0100 @@ -37,45 +37,45 @@ (** markup commands **) val headerP = OuterSyntax.markup_command IsarOutput.Markup "header" "theory header" K.diag - (P.comment >> IsarThy.add_header); + (P.text >> IsarThy.add_header); val chapterP = OuterSyntax.markup_command IsarOutput.Markup "chapter" "chapter heading" - K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_chapter)); + K.thy_heading (P.text >> (Toplevel.theory o IsarThy.add_chapter)); val sectionP = OuterSyntax.markup_command IsarOutput.Markup "section" "section heading" - K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_section)); + K.thy_heading (P.text >> (Toplevel.theory o IsarThy.add_section)); val subsectionP = OuterSyntax.markup_command IsarOutput.Markup "subsection" "subsection heading" - K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_subsection)); + K.thy_heading (P.text >> (Toplevel.theory o IsarThy.add_subsection)); val subsubsectionP = OuterSyntax.markup_command IsarOutput.Markup "subsubsection" "subsubsection heading" - K.thy_heading (P.comment >> (Toplevel.theory o IsarThy.add_subsubsection)); + K.thy_heading (P.text >> (Toplevel.theory o IsarThy.add_subsubsection)); val textP = OuterSyntax.markup_command IsarOutput.MarkupEnv "text" "formal comment (theory)" - K.thy_decl (P.comment >> (Toplevel.theory o IsarThy.add_text)); + K.thy_decl (P.text >> (Toplevel.theory o IsarThy.add_text)); val text_rawP = OuterSyntax.markup_command IsarOutput.Verbatim "text_raw" "raw document preparation text" K.thy_decl - (P.comment >> (Toplevel.theory o IsarThy.add_text_raw)); + (P.text >> (Toplevel.theory o IsarThy.add_text_raw)); val sectP = OuterSyntax.markup_command IsarOutput.Markup "sect" "formal comment (proof)" - K.prf_heading (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect))); + K.prf_heading (P.text >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_sect))); val subsectP = OuterSyntax.markup_command IsarOutput.Markup "subsect" "formal comment (proof)" - K.prf_heading (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect))); + K.prf_heading (P.text >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsect))); val subsubsectP = OuterSyntax.markup_command IsarOutput.Markup "subsubsect" "formal comment (proof)" K.prf_heading - (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect))); + (P.text >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_subsubsect))); val txtP = OuterSyntax.markup_command IsarOutput.MarkupEnv "txt" "formal comment (proof)" - K.prf_decl (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt))); + K.prf_decl (P.text >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt))); val txt_rawP = OuterSyntax.markup_command IsarOutput.Verbatim "txt_raw" "raw document preparation text (proof)" K.prf_decl - (P.comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt_raw))); + (P.text >> (Toplevel.print oo (Toplevel.proof o IsarThy.add_txt_raw))); @@ -86,53 +86,51 @@ val classesP = OuterSyntax.command "classes" "declare type classes" K.thy_decl (Scan.repeat1 (P.name -- Scan.optional ((P.$$$ "\\" || P.$$$ "<") |-- - P.!!! (P.list1 P.xname)) []) - -- P.marg_comment >> (Toplevel.theory o IsarThy.add_classes)); + P.!!! (P.list1 P.xname)) []) >> (Toplevel.theory o Theory.add_classes)); val classrelP = OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl - (P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) -- P.marg_comment - >> (Toplevel.theory o IsarThy.add_classrel)); + (P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) + >> (Toplevel.theory o Theory.add_classrel o single)); val defaultsortP = OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl - (P.sort -- P.marg_comment >> (Toplevel.theory o IsarThy.add_defsort)); + (P.sort >> (Toplevel.theory o Theory.add_defsort)); (* types *) val typedeclP = OuterSyntax.command "typedecl" "type declaration" K.thy_decl - (P.type_args -- P.name -- P.opt_infix -- P.marg_comment >> (fn (((args, a), mx), cmt) => - Toplevel.theory (IsarThy.add_typedecl ((a, args, mx), cmt)))); + (P.type_args -- P.name -- P.opt_infix >> (fn ((args, a), mx) => + Toplevel.theory (PureThy.add_typedecls [(a, args, mx)]))); val typeabbrP = OuterSyntax.command "types" "declare type abbreviations" K.thy_decl (Scan.repeat1 - (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix')) -- P.marg_comment) - >> (Toplevel.theory o IsarThy.add_tyabbrs o - map (fn (((args, a), (T, mx)), cmt) => ((a, args, T, mx), cmt)))); + (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix'))) + >> (Toplevel.theory o Theory.add_tyabbrs o + map (fn ((args, a), (T, mx)) => (a, args, T, mx)))); val nontermP = OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols" - K.thy_decl (Scan.repeat1 (P.name -- P.marg_comment) - >> (Toplevel.theory o IsarThy.add_nonterminals)); + K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Theory.add_nonterminals)); val aritiesP = OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl - (Scan.repeat1 ((P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2) -- P.marg_comment) - >> (Toplevel.theory o IsarThy.add_arities)); + (Scan.repeat1 (P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2) + >> (Toplevel.theory o Theory.add_arities)); (* consts and syntax *) val judgmentP = OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl - (P.const -- P.marg_comment >> (Toplevel.theory o IsarThy.add_judgment)); + (P.const >> (Toplevel.theory o ObjectLogic.add_judgment)); val constsP = OuterSyntax.command "consts" "declare constants" K.thy_decl - (Scan.repeat1 (P.const -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_consts)); + (Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts)); val mode_spec = @@ -142,8 +140,7 @@ val syntaxP = OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl - (opt_mode -- Scan.repeat1 (P.const -- P.marg_comment) - >> (Toplevel.theory o uncurry IsarThy.add_modesyntax)); + (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.add_modesyntax)); (* translations *) @@ -162,33 +159,31 @@ val translationsP = OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl - (Scan.repeat1 (trans_line -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_trrules)); + (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules)); (* axioms and definitions *) val axiomsP = OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl - (Scan.repeat1 (P.spec_name -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_axioms)); + (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_axioms)); val opt_overloaded = Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false; val defsP = OuterSyntax.command "defs" "define constants" K.thy_decl - (opt_overloaded -- Scan.repeat1 (P.spec_name -- P.marg_comment) - >> (Toplevel.theory o IsarThy.add_defs)); + (opt_overloaded -- Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_defs)); val constdefsP = OuterSyntax.command "constdefs" "declare and define constants" K.thy_decl - (Scan.repeat1 ((P.const -- P.marg_comment) -- (P.term -- P.marg_comment)) - >> (Toplevel.theory o IsarThy.add_constdefs)); + (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o IsarThy.add_constdefs)); (* theorems *) val in_locale = Scan.option ((P.$$$ "(" -- P.$$$ "in") |-- P.!!! (P.xname --| P.$$$ ")")); -val name_facts = P.and_list1 (P.opt_thm_name "=" -- P.xthms1 -- P.marg_comment); +val name_facts = P.and_list1 (P.opt_thm_name "=" -- P.xthms1); fun theorems kind = in_locale -- name_facts >> uncurry (#1 ooo IsarThy.smart_theorems kind); @@ -203,93 +198,92 @@ val declareP = OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script - (in_locale -- (P.xthms1 -- P.marg_comment) - >> (Toplevel.theory o uncurry IsarThy.declare_theorems)); + (in_locale -- P.xthms1 >> (Toplevel.theory o uncurry IsarThy.declare_theorems)); (* name space entry path *) val globalP = OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl - (P.marg_comment >> (Toplevel.theory o IsarThy.global_path)); + (Scan.succeed (Toplevel.theory PureThy.global_path)); val localP = OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl - (P.marg_comment >> (Toplevel.theory o IsarThy.local_path)); + (Scan.succeed (Toplevel.theory PureThy.local_path)); val hideP = OuterSyntax.command "hide" "hide names from given name space" K.thy_decl - (P.name -- Scan.repeat1 P.xname -- P.marg_comment >> (Toplevel.theory o IsarThy.hide_space)); + (P.name -- Scan.repeat1 P.xname >> (Toplevel.theory o IsarThy.hide_space)); (* use ML text *) val useP = OuterSyntax.command "use" "eval ML text from file" K.diag - (P.name -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.use)); + (P.name >> (Toplevel.no_timing oo IsarCmd.use)); val mlP = OuterSyntax.command "ML" "eval ML text (diagnostic)" K.diag - (P.text -- P.marg_comment >> IsarCmd.use_mltext true); + (P.text >> IsarCmd.use_mltext true); val ml_commandP = OuterSyntax.command "ML_command" "eval ML text" K.diag - (P.text -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.use_mltext false)); + (P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false)); val ml_setupP = OuterSyntax.command "ML_setup" "eval ML text (may change theory)" K.thy_decl - (P.text -- P.marg_comment >> IsarCmd.use_mltext_theory); + (P.text >> IsarCmd.use_mltext_theory); val setupP = OuterSyntax.command "setup" "apply ML theory setup" K.thy_decl - (P.text -- P.marg_comment >> (Toplevel.theory o IsarCmd.use_setup)); + (P.text >> (Toplevel.theory o Context.use_setup)); val method_setupP = OuterSyntax.command "method_setup" "define proof method in ML" K.thy_decl - (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2) - -- P.marg_comment) >> (Toplevel.theory o IsarThy.method_setup)); + (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2)) + >> (Toplevel.theory o IsarThy.method_setup)); (* translation functions *) val parse_ast_translationP = OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" K.thy_decl - (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.parse_ast_translation)); + (P.text >> (Toplevel.theory o IsarThy.parse_ast_translation)); val parse_translationP = OuterSyntax.command "parse_translation" "install parse translation functions" K.thy_decl - (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.parse_translation)); + (P.text >> (Toplevel.theory o IsarThy.parse_translation)); val print_translationP = OuterSyntax.command "print_translation" "install print translation functions" K.thy_decl - (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.print_translation)); + (P.text >> (Toplevel.theory o IsarThy.print_translation)); val typed_print_translationP = OuterSyntax.command "typed_print_translation" "install typed print translation functions" - K.thy_decl (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.typed_print_translation)); + K.thy_decl (P.text >> (Toplevel.theory o IsarThy.typed_print_translation)); val print_ast_translationP = OuterSyntax.command "print_ast_translation" "install print ast translation functions" K.thy_decl - (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.print_ast_translation)); + (P.text >> (Toplevel.theory o IsarThy.print_ast_translation)); val token_translationP = OuterSyntax.command "token_translation" "install token translation functions" K.thy_decl - (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.token_translation)); + (P.text >> (Toplevel.theory o IsarThy.token_translation)); (* oracles *) val oracleP = OuterSyntax.command "oracle" "install oracle" K.thy_decl - ((P.name --| P.$$$ "=") -- P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.add_oracle)); + ((P.name --| P.$$$ "=") -- P.text >> (Toplevel.theory o IsarThy.add_oracle)); (* locales *) val locale_val = (P.locale_expr -- - Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 (P.locale_element -- P.marg_comment))) [] || - Scan.repeat1 (P.locale_element -- P.marg_comment) >> pair Locale.empty); + Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.locale_element)) [] || + Scan.repeat1 P.locale_element >> pair Locale.empty); val localeP = OuterSyntax.command "locale" "define named proof context" K.thy_decl @@ -305,7 +299,7 @@ val in_locale_elems = in_locale -- Scan.optional (P.$$$ "(" |-- Scan.repeat1 P.locale_element --| P.!!! (P.$$$ ")")) []; -val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment); +val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp); val statement' = P.$$$ "(" |-- statement --| P.!!! (P.$$$ ")") || statement; fun gen_theorem k = @@ -337,11 +331,11 @@ (* facts *) -val facts = P.and_list1 (P.xthms1 -- P.marg_comment); +val facts = P.and_list1 P.xthms1; val thenP = OuterSyntax.command "then" "forward chaining" K.prf_chain - (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.chain))); + (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.chain))); val fromP = OuterSyntax.command "from" "forward chaining from given facts" K.prf_chain @@ -360,7 +354,7 @@ val fixP = OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm - (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment) + (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ)) >> (Toplevel.print oo (Toplevel.proof o IsarThy.fix))); val assumeP = @@ -374,19 +368,19 @@ val defP = OuterSyntax.command "def" "local definition" K.prf_asm (P.opt_thm_name ":" -- (P.name -- ((P.$$$ "\\" || P.$$$ "==") |-- P.!!! P.termp)) - -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def))); + >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def))); val obtainP = OuterSyntax.command "obtain" "generalized existence" K.prf_asm_goal (Scan.optional - (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment) + (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ)) --| P.$$$ "where") [] -- statement >> (Toplevel.print oo (Toplevel.proof o IsarThy.obtain))); val letP = OuterSyntax.command "let" "bind text variables" K.prf_decl - (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment) + (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term)) >> (Toplevel.print oo (Toplevel.proof o IsarThy.let_bind))); val case_spec = @@ -395,109 +389,105 @@ val caseP = OuterSyntax.command "case" "invoke local context" K.prf_asm - (case_spec -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case))); + (case_spec >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case))); (* proof structure *) val beginP = OuterSyntax.command "{" "begin explicit proof block" K.prf_open - (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.begin_block))); + (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.begin_block))); val endP = OuterSyntax.command "}" "end explicit proof block" K.prf_close - (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.end_block))); + (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.end_block))); val nextP = OuterSyntax.command "next" "enter next proof block" K.prf_block - (P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.next_block))); + (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.next_block))); (* end proof *) val qedP = OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block - (Scan.option (P.method -- P.interest) -- P.marg_comment >> IsarThy.qed); + (Scan.option P.method >> IsarThy.qed); val terminal_proofP = OuterSyntax.command "by" "terminal backward proof" K.qed - (P.method -- P.interest -- Scan.option (P.method -- P.interest) - -- P.marg_comment >> IsarThy.terminal_proof); + (P.method -- Scan.option P.method >> IsarThy.terminal_proof); val default_proofP = OuterSyntax.command ".." "default proof" K.qed - (P.marg_comment >> IsarThy.default_proof); + (Scan.succeed IsarThy.default_proof); val immediate_proofP = OuterSyntax.command "." "immediate proof" K.qed - (P.marg_comment >> IsarThy.immediate_proof); + (Scan.succeed IsarThy.immediate_proof); val done_proofP = OuterSyntax.command "done" "done proof" K.qed - (P.marg_comment >> IsarThy.done_proof); + (Scan.succeed IsarThy.done_proof); val skip_proofP = OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed - (P.marg_comment >> IsarThy.skip_proof); + (Scan.succeed IsarThy.skip_proof); val forget_proofP = OuterSyntax.command "oops" "forget proof" K.qed_global - (P.marg_comment >> IsarThy.forget_proof); - + (Scan.succeed IsarThy.forget_proof); (* proof steps *) val deferP = OuterSyntax.command "defer" "shuffle internal proof state" K.prf_script - (Scan.option P.nat -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.defer))); + (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.defer))); val preferP = OuterSyntax.command "prefer" "shuffle internal proof state" K.prf_script - (P.nat -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.prefer))); + (P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.prefer))); val applyP = OuterSyntax.command "apply" "initial refinement step (unstructured)" K.prf_script - (P.method -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply))); + (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply))); val apply_endP = OuterSyntax.command "apply_end" "terminal refinement (unstructured)" K.prf_script - (P.method -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply_end))); + (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply_end))); val proofP = OuterSyntax.command "proof" "backward proof" K.prf_block - (P.interest -- Scan.option (P.method -- P.interest) -- P.marg_comment - >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof))); + (Scan.option P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof))); (* calculational proof commands *) val calc_args = - Scan.option (P.$$$ "(" |-- P.!!! ((P.xthms1 --| P.$$$ ")") -- P.interest)); + Scan.option (P.$$$ "(" |-- P.!!! ((P.xthms1 --| P.$$$ ")"))); val alsoP = OuterSyntax.command "also" "combine calculation and current facts" K.prf_decl - (calc_args -- P.marg_comment >> IsarThy.also); + (calc_args >> IsarThy.also); val finallyP = OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" K.prf_chain - (calc_args -- P.marg_comment >> IsarThy.finally); + (calc_args >> IsarThy.finally); val moreoverP = OuterSyntax.command "moreover" "augment calculation by current facts" K.prf_decl - (P.marg_comment >> IsarThy.moreover); + (Scan.succeed IsarThy.moreover); val ultimatelyP = OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result" - K.prf_chain (P.marg_comment >> IsarThy.ultimately); + K.prf_chain (Scan.succeed IsarThy.ultimately); (* proof navigation *) val backP = OuterSyntax.command "back" "backtracking of proof command" K.prf_script - (Scan.optional (P.$$$ "!" >> K true) false -- P.marg_comment >> - (Toplevel.print oo IsarCmd.back)); + (Scan.optional (P.$$$ "!" >> K true) false >> (Toplevel.print oo IsarCmd.back)); (* history *) @@ -611,29 +601,27 @@ val print_thmsP = OuterSyntax.improper_command "thm" "print theorems" K.diag - (opt_modes -- P.xthms1 -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_thms)); + (opt_modes -- P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms)); val print_prfsP = OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag - (opt_modes -- Scan.option P.xthms1 -- P.marg_comment >> - (Toplevel.no_timing oo IsarCmd.print_prfs false)); + (opt_modes -- Scan.option P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs false)); val print_full_prfsP = OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag - (opt_modes -- Scan.option P.xthms1 -- P.marg_comment >> - (Toplevel.no_timing oo IsarCmd.print_prfs true)); + (opt_modes -- Scan.option P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true)); val print_propP = OuterSyntax.improper_command "prop" "read and print proposition" K.diag - (opt_modes -- P.term -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_prop)); + (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_prop)); val print_termP = OuterSyntax.improper_command "term" "read and print term" K.diag - (opt_modes -- P.term -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_term)); + (opt_modes -- P.term >> (Toplevel.no_timing oo IsarCmd.print_term)); val print_typeP = OuterSyntax.improper_command "typ" "read and print type" K.diag - (opt_modes -- P.typ -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.print_type)); + (opt_modes -- P.typ >> (Toplevel.no_timing oo IsarCmd.print_type)); diff -r bda60442bf02 -r a70df1e5bf10 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/Pure/Isar/isar_thy.ML Tue Feb 12 20:28:27 2002 +0100 @@ -8,206 +8,154 @@ signature ISAR_THY = sig - val add_header: Comment.text -> Toplevel.transition -> Toplevel.transition - val add_chapter: Comment.text -> theory -> theory - val add_section: Comment.text -> theory -> theory - val add_subsection: Comment.text -> theory -> theory - val add_subsubsection: Comment.text -> theory -> theory - val add_text: Comment.text -> theory -> theory - val add_text_raw: Comment.text -> theory -> theory - val add_sect: Comment.text -> ProofHistory.T -> ProofHistory.T - val add_subsect: Comment.text -> ProofHistory.T -> ProofHistory.T - val add_subsubsect: Comment.text -> ProofHistory.T -> ProofHistory.T - val add_txt: Comment.text -> ProofHistory.T -> ProofHistory.T - val add_txt_raw: Comment.text -> ProofHistory.T -> ProofHistory.T - val global_path: Comment.text -> theory -> theory - val local_path: Comment.text -> theory -> theory - val hide_space: (string * xstring list) * Comment.text -> theory -> theory - val hide_space_i: (string * string list) * Comment.text -> theory -> theory - val add_classes: (bclass * xclass list) list * Comment.text -> theory -> theory - val add_classes_i: (bclass * class list) list * Comment.text -> theory -> theory - val add_classrel: (xclass * xclass) * Comment.text -> theory -> theory - val add_classrel_i: (class * class) * Comment.text -> theory -> theory - val add_defsort: string * Comment.text -> theory -> theory - val add_defsort_i: sort * Comment.text -> theory -> theory - val add_nonterminals: (bstring * Comment.text) list -> theory -> theory - val add_tyabbrs: ((bstring * string list * string * mixfix) * Comment.text) list - -> theory -> theory - val add_tyabbrs_i: ((bstring * string list * typ * mixfix) * Comment.text) list - -> theory -> theory - val add_arities: ((xstring * string list * string) * Comment.text) list -> theory -> theory - val add_arities_i: ((string * sort list * sort) * Comment.text) list -> theory -> theory - val add_typedecl: (bstring * string list * mixfix) * Comment.text -> theory -> theory - val add_consts: ((bstring * string * mixfix) * Comment.text) list -> theory -> theory - val add_consts_i: ((bstring * typ * mixfix) * Comment.text) list -> theory -> theory - val add_modesyntax: string * bool -> ((bstring * string * mixfix) * Comment.text) list - -> theory -> theory - val add_modesyntax_i: string * bool -> ((bstring * typ * mixfix) * Comment.text) list - -> theory -> theory - val add_trrules: ((xstring * string) Syntax.trrule * Comment.text) list -> theory -> theory - val add_trrules_i: (Syntax.ast Syntax.trrule * Comment.text) list -> theory -> theory - val add_judgment: (bstring * string * mixfix) * Comment.text -> theory -> theory - val add_judgment_i: (bstring * typ * mixfix) * Comment.text -> theory -> theory - val add_axioms: (((bstring * string) * Args.src list) * Comment.text) list -> theory -> theory - val add_axioms_i: (((bstring * term) * theory attribute list) * Comment.text) list - -> theory -> theory - val add_defs: bool * (((bstring * string) * Args.src list) * Comment.text) list - -> theory -> theory - val add_defs_i: bool * (((bstring * term) * theory attribute list) * Comment.text) list - -> theory -> theory - val add_constdefs: (((bstring * string * mixfix) * Comment.text) * (string * Comment.text)) list - -> theory -> theory - val add_constdefs_i: (((bstring * typ * mixfix) * Comment.text) * (term * Comment.text)) list - -> theory -> theory - val theorems: string -> - (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list + val add_header: string -> Toplevel.transition -> Toplevel.transition + val add_chapter: string -> theory -> theory + val add_section: string -> theory -> theory + val add_subsection: string -> theory -> theory + val add_subsubsection: string -> theory -> theory + val add_text: string -> theory -> theory + val add_text_raw: string -> theory -> theory + val add_sect: string -> ProofHistory.T -> ProofHistory.T + val add_subsect: string -> ProofHistory.T -> ProofHistory.T + val add_subsubsect: string -> ProofHistory.T -> ProofHistory.T + val add_txt: string -> ProofHistory.T -> ProofHistory.T + val add_txt_raw: string -> ProofHistory.T -> ProofHistory.T + val hide_space: string * xstring list -> theory -> theory + val hide_space_i: string * string list -> theory -> theory + val add_axioms: ((bstring * string) * Args.src list) list -> theory -> theory + val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory + val add_defs: bool * ((bstring * string) * Args.src list) list -> theory -> theory + val add_defs_i: bool * ((bstring * term) * theory attribute list) list -> theory -> theory + val add_constdefs: ((bstring * string * mixfix) * string) list -> theory -> theory + val add_constdefs_i: ((bstring * typ * mixfix) * term) list -> theory -> theory + val theorems: string -> ((bstring * Args.src list) * (xstring * Args.src list) list) list -> theory -> theory * (string * thm list) list val theorems_i: string -> - (((bstring * theory attribute list) - * (thm list * theory attribute list) list) * Comment.text) list + ((bstring * theory attribute list) * (thm list * theory attribute list) list) list -> theory -> theory * (string * thm list) list val locale_theorems: string -> xstring -> - (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list + ((bstring * Args.src list) * (xstring * Args.src list) list) list -> theory -> theory * (bstring * thm list) list val locale_theorems_i: string -> string -> - (((bstring * Proof.context attribute list) - * (thm list * Proof.context attribute list) list) * Comment.text) list + ((bstring * Proof.context attribute list) + * (thm list * Proof.context attribute list) list) list -> theory -> theory * (string * thm list) list val smart_theorems: string -> xstring option -> - (((bstring * Args.src list) * (xstring * Args.src list) list) * Comment.text) list + ((bstring * Args.src list) * (xstring * Args.src list) list) list -> theory -> theory * (string * thm list) list - val declare_theorems: xstring option -> (xstring * Args.src list) list * Comment.text - -> theory -> theory + val declare_theorems: xstring option -> (xstring * Args.src list) list -> theory -> theory val apply_theorems: (xstring * Args.src list) list -> theory -> theory * thm list val apply_theorems_i: (thm list * theory attribute list) list -> theory -> theory * thm list - val have_facts: (((string * Args.src list) * (string * Args.src list) list) * Comment.text) list - -> ProofHistory.T -> ProofHistory.T - val have_facts_i: (((string * Proof.context attribute list) * - (thm * Proof.context attribute list) list) * Comment.text) list + val have_facts: ((string * Args.src list) * (string * Args.src list) list) list -> ProofHistory.T -> ProofHistory.T - val from_facts: ((string * Args.src list) list * Comment.text) list - -> ProofHistory.T -> ProofHistory.T - val from_facts_i: ((thm * Proof.context attribute list) list * Comment.text) list + val have_facts_i: ((string * Proof.context attribute list) * + (thm * Proof.context attribute list) list) list -> ProofHistory.T -> ProofHistory.T + val from_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T + val from_facts_i: (thm * Proof.context attribute list) list list -> ProofHistory.T -> ProofHistory.T - val with_facts: ((string * Args.src list) list * Comment.text) list - -> ProofHistory.T -> ProofHistory.T - val with_facts_i: ((thm * Proof.context attribute list) list * Comment.text) list + val with_facts: (string * Args.src list) list list -> ProofHistory.T -> ProofHistory.T + val with_facts_i: (thm * Proof.context attribute list) list list -> ProofHistory.T -> ProofHistory.T - val chain: Comment.text -> ProofHistory.T -> ProofHistory.T - val fix: ((string list * string option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T - val fix_i: ((string list * typ option) * Comment.text) list -> ProofHistory.T -> ProofHistory.T - val let_bind: ((string list * string) * Comment.text) list -> ProofHistory.T -> ProofHistory.T - val let_bind_i: ((term list * term) * Comment.text) list -> ProofHistory.T -> ProofHistory.T - val invoke_case: (string * string option list * Args.src list) * Comment.text + val chain: ProofHistory.T -> ProofHistory.T + val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T + val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T + val let_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T + val let_bind_i: (term list * term) list -> ProofHistory.T -> ProofHistory.T + val invoke_case: string * string option list * Args.src list -> ProofHistory.T -> ProofHistory.T + val invoke_case_i: string * string option list * Proof.context attribute list -> ProofHistory.T -> ProofHistory.T - val invoke_case_i: (string * string option list * Proof.context attribute list) * Comment.text - -> ProofHistory.T -> ProofHistory.T - val theorem: string - -> ((bstring * Args.src list) * (string * (string list * string list))) * Comment.text + val theorem: string -> (bstring * Args.src list) * (string * (string list * string list)) -> bool -> theory -> ProofHistory.T - val theorem_i: string -> ((bstring * theory attribute list) * - (term * (term list * term list))) * Comment.text -> bool -> theory -> ProofHistory.T + val theorem_i: string -> (bstring * theory attribute list) * + (term * (term list * term list)) -> bool -> theory -> ProofHistory.T val multi_theorem: string -> bstring * Args.src list -> Args.src Locale.element list -> - (((bstring * Args.src list) * (string * (string list * string list)) list) - * Comment.text) list -> bool -> theory -> ProofHistory.T + ((bstring * Args.src list) * (string * (string list * string list)) list) list + -> bool -> theory -> ProofHistory.T val multi_theorem_i: string -> bstring * theory attribute list -> Proof.context attribute Locale.element_i list -> - (((bstring * theory attribute list) * (term * (term list * term list)) list) - * Comment.text) list -> bool -> theory -> ProofHistory.T + ((bstring * theory attribute list) * (term * (term list * term list)) list) list + -> bool -> theory -> ProofHistory.T val locale_multi_theorem: string -> bstring * Args.src list -> xstring -> Args.src Locale.element list -> - (((bstring * Args.src list) * (string * (string list * string list)) list) - * Comment.text) list -> bool -> theory -> ProofHistory.T + ((bstring * Args.src list) * (string * (string list * string list)) list) list + -> bool -> theory -> ProofHistory.T val locale_multi_theorem_i: string -> bstring * theory attribute list -> string -> Proof.context attribute Locale.element_i list -> - (((bstring * Proof.context attribute list) * (term * (term list * term list)) list) - * Comment.text) list -> bool -> theory -> ProofHistory.T + ((bstring * Proof.context attribute list) * (term * (term list * term list)) list) list + -> bool -> theory -> ProofHistory.T val smart_multi_theorem: string -> bstring * Args.src list -> xstring Library.option * Args.src Locale.element list -> - (((bstring * Args.src list) * (string * (string list * string list)) list) - * Comment.text) list -> bool -> theory -> ProofHistory.T - val assume: (((string * Args.src list) * (string * (string list * string list)) list) - * Comment.text) list -> ProofHistory.T -> ProofHistory.T - val assume_i: (((string * Proof.context attribute list) * (term * (term list * term list)) list) - * Comment.text) list -> ProofHistory.T -> ProofHistory.T - val presume: (((string * Args.src list) * (string * (string list * string list)) list) - * Comment.text) list -> ProofHistory.T -> ProofHistory.T - val presume_i: (((string * Proof.context attribute list) * (term * (term list * term list)) list) - * Comment.text) list -> ProofHistory.T -> ProofHistory.T - val have: (((string * Args.src list) * - (string * (string list * string list)) list) * Comment.text) list + ((bstring * Args.src list) * (string * (string list * string list)) list) list + -> bool -> theory -> ProofHistory.T + val assume: ((string * Args.src list) * (string * (string list * string list)) list) list -> ProofHistory.T -> ProofHistory.T - val have_i: (((string * Proof.context attribute list) * - (term * (term list * term list)) list) * Comment.text) list + val assume_i: + ((string * Proof.context attribute list) * (term * (term list * term list)) list) list + -> ProofHistory.T -> ProofHistory.T + val presume: ((string * Args.src list) * (string * (string list * string list)) list) list + -> ProofHistory.T -> ProofHistory.T + val presume_i: + ((string * Proof.context attribute list) * (term * (term list * term list)) list) list -> ProofHistory.T -> ProofHistory.T - val hence: (((string * Args.src list) * - (string * (string list * string list)) list) * Comment.text) list + val have: ((string * Args.src list) * (string * (string list * string list)) list) list -> ProofHistory.T -> ProofHistory.T - val hence_i: (((string * Proof.context attribute list) * - (term * (term list * term list)) list) * Comment.text) list + val have_i: ((string * Proof.context attribute list) * + (term * (term list * term list)) list) list -> ProofHistory.T -> ProofHistory.T + val hence: ((string * Args.src list) * (string * (string list * string list)) list) list -> ProofHistory.T -> ProofHistory.T - val show: (((string * Args.src list) * - (string * (string list * string list)) list) * Comment.text) list + val hence_i: ((string * Proof.context attribute list) * + (term * (term list * term list)) list) list -> ProofHistory.T -> ProofHistory.T + val show: ((string * Args.src list) * (string * (string list * string list)) list) list -> bool -> ProofHistory.T -> ProofHistory.T - val show_i: (((string * Proof.context attribute list) * - (term * (term list * term list)) list) * Comment.text) list - -> bool -> ProofHistory.T -> ProofHistory.T - val thus: (((string * Args.src list) * - (string * (string list * string list)) list) * Comment.text) list - -> bool -> ProofHistory.T -> ProofHistory.T - val thus_i: (((string * Proof.context attribute list) * - (term * (term list * term list)) list) * Comment.text) list + val show_i: ((string * Proof.context attribute list) * + (term * (term list * term list)) list) list -> bool -> ProofHistory.T -> ProofHistory.T + val thus: ((string * Args.src list) * (string * (string list * string list)) list) list -> bool -> ProofHistory.T -> ProofHistory.T - val local_def: ((string * Args.src list) * (string * (string * string list))) - * Comment.text -> ProofHistory.T -> ProofHistory.T - val local_def_i: ((string * Args.src list) * (string * (term * term list))) - * Comment.text -> ProofHistory.T -> ProofHistory.T - val obtain: ((string list * string option) * Comment.text) list - * (((string * Args.src list) * (string * (string list * string list)) list) - * Comment.text) list -> ProofHistory.T -> ProofHistory.T - val obtain_i: ((string list * typ option) * Comment.text) list - * (((string * Proof.context attribute list) * (term * (term list * term list)) list) - * Comment.text) list -> ProofHistory.T -> ProofHistory.T - val begin_block: Comment.text -> ProofHistory.T -> ProofHistory.T - val next_block: Comment.text -> ProofHistory.T -> ProofHistory.T - val end_block: Comment.text -> ProofHistory.T -> ProofHistory.T - val defer: int option * Comment.text -> ProofHistory.T -> ProofHistory.T - val prefer: int * Comment.text -> ProofHistory.T -> ProofHistory.T - val apply: Method.text * Comment.text -> ProofHistory.T -> ProofHistory.T - val apply_end: Method.text * Comment.text -> ProofHistory.T -> ProofHistory.T - val proof: (Comment.interest * (Method.text * Comment.interest) option) * Comment.text + val thus_i: ((string * Proof.context attribute list) + * (term * (term list * term list)) list) list -> bool -> ProofHistory.T -> ProofHistory.T + val local_def: (string * Args.src list) * (string * (string * string list)) + -> ProofHistory.T -> ProofHistory.T + val local_def_i: (string * Args.src list) * (string * (term * term list)) + -> ProofHistory.T -> ProofHistory.T + val obtain: (string list * string option) list + * ((string * Args.src list) * (string * (string list * string list)) list) list -> ProofHistory.T -> ProofHistory.T - val qed: (Method.text * Comment.interest) option * Comment.text + val obtain_i: (string list * typ option) list + * ((string * Proof.context attribute list) * (term * (term list * term list)) list) list + -> ProofHistory.T -> ProofHistory.T + val begin_block: ProofHistory.T -> ProofHistory.T + val next_block: ProofHistory.T -> ProofHistory.T + val end_block: ProofHistory.T -> ProofHistory.T + val defer: int option -> ProofHistory.T -> ProofHistory.T + val prefer: int -> ProofHistory.T -> ProofHistory.T + val apply: Method.text -> ProofHistory.T -> ProofHistory.T + val apply_end: Method.text -> ProofHistory.T -> ProofHistory.T + val proof: Method.text option -> ProofHistory.T -> ProofHistory.T + val qed: Method.text option -> Toplevel.transition -> Toplevel.transition + val terminal_proof: Method.text * Method.text option -> Toplevel.transition -> Toplevel.transition - val terminal_proof: ((Method.text * Comment.interest) * (Method.text * Comment.interest) option) - * Comment.text -> Toplevel.transition -> Toplevel.transition - val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition - val immediate_proof: Comment.text -> Toplevel.transition -> Toplevel.transition - val done_proof: Comment.text -> Toplevel.transition -> Toplevel.transition - val skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition - val forget_proof: Comment.text -> Toplevel.transition -> Toplevel.transition + val default_proof: Toplevel.transition -> Toplevel.transition + val immediate_proof: Toplevel.transition -> Toplevel.transition + val done_proof: Toplevel.transition -> Toplevel.transition + val skip_proof: Toplevel.transition -> Toplevel.transition + val forget_proof: Toplevel.transition -> Toplevel.transition val get_thmss: (string * Args.src list) list -> Proof.state -> thm list - val also: ((string * Args.src list) list * Comment.interest) option * Comment.text - -> Toplevel.transition -> Toplevel.transition - val also_i: (thm list * Comment.interest) option * Comment.text - -> Toplevel.transition -> Toplevel.transition - val finally: ((string * Args.src list) list * Comment.interest) option * Comment.text - -> Toplevel.transition -> Toplevel.transition - val finally_i: (thm list * Comment.interest) option * Comment.text - -> Toplevel.transition -> Toplevel.transition - val moreover: Comment.text -> Toplevel.transition -> Toplevel.transition - val ultimately: Comment.text -> Toplevel.transition -> Toplevel.transition - val parse_ast_translation: string * Comment.text -> theory -> theory - val parse_translation: string * Comment.text -> theory -> theory - val print_translation: string * Comment.text -> theory -> theory - val typed_print_translation: string * Comment.text -> theory -> theory - val print_ast_translation: string * Comment.text -> theory -> theory - val token_translation: string * Comment.text -> theory -> theory - val method_setup: (bstring * string * string) * Comment.text -> theory -> theory - val add_oracle: (bstring * string) * Comment.text -> theory -> theory - val add_locale: bstring * Locale.expr * (Args.src Locale.element * Comment.text) list - -> theory -> theory + val also: (string * Args.src list) list option -> Toplevel.transition -> Toplevel.transition + val also_i: thm list option -> Toplevel.transition -> Toplevel.transition + val finally: (string * Args.src list) list option -> Toplevel.transition -> Toplevel.transition + val finally_i: thm list option -> Toplevel.transition -> Toplevel.transition + val moreover: Toplevel.transition -> Toplevel.transition + val ultimately: Toplevel.transition -> Toplevel.transition + val parse_ast_translation: string -> theory -> theory + val parse_translation: string -> theory -> theory + val print_translation: string -> theory -> theory + val typed_print_translation: string -> theory -> theory + val print_ast_translation: string -> theory -> theory + val token_translation: string -> theory -> theory + val method_setup: bstring * string * string -> theory -> theory + val add_oracle: bstring * string -> theory -> theory + val add_locale: bstring * Locale.expr * Args.src Locale.element list -> theory -> theory val begin_theory: string -> string list -> (string * bool) list -> theory val end_theory: theory -> theory val kill_theory: string -> unit @@ -225,21 +173,20 @@ (* markup commands *) -fun add_header comment = +fun add_header x = Toplevel.keep (fn state => if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF); fun add_text _ x = x; fun add_text_raw _ x = x; -fun add_heading add present txt thy = - (Context.setmp (Some thy) present (Comment.string_of txt); add txt thy); +fun add_heading add present txt thy = (Context.setmp (Some thy) present txt; add txt thy); val add_chapter = add_heading add_text Present.section; val add_section = add_heading add_text Present.section; val add_subsection = add_heading add_text Present.subsection; val add_subsubsection = add_heading add_text Present.subsubsection; -fun add_txt (_: Comment.text) = ProofHistory.apply I; +fun add_txt (_: string) = ProofHistory.apply I; val add_txt_raw = add_txt; val add_sect = add_txt; val add_subsect = add_txt; @@ -248,9 +195,6 @@ (* name spaces *) -fun global_path comment_ignore = PureThy.global_path; -fun local_path comment_ignore = PureThy.local_path; - local val kinds = @@ -259,7 +203,7 @@ can (Sign.certify_tycon sg) c orelse can (Sign.certify_tyabbr sg) c), (Sign.constK, can o Sign.certify_const)]; -fun gen_hide intern ((kind, xnames), comment_ignore) thy = +fun gen_hide intern (kind, xnames) thy = (case assoc (kinds, kind) of Some check => let @@ -280,51 +224,27 @@ end; -(* signature and syntax *) - -val add_classes = Theory.add_classes o Comment.ignore; -val add_classes_i = Theory.add_classes_i o Comment.ignore; -val add_classrel = Theory.add_classrel o single o Comment.ignore; -val add_classrel_i = Theory.add_classrel_i o single o Comment.ignore; -val add_defsort = Theory.add_defsort o Comment.ignore; -val add_defsort_i = Theory.add_defsort_i o Comment.ignore; -val add_nonterminals = Theory.add_nonterminals o map Comment.ignore; -val add_tyabbrs = Theory.add_tyabbrs o map Comment.ignore; -val add_tyabbrs_i = Theory.add_tyabbrs_i o map Comment.ignore; -val add_arities = Theory.add_arities o map Comment.ignore; -val add_arities_i = Theory.add_arities_i o map Comment.ignore; -val add_typedecl = PureThy.add_typedecls o single o Comment.ignore; -val add_consts = Theory.add_consts o map Comment.ignore; -val add_consts_i = Theory.add_consts_i o map Comment.ignore; -fun add_modesyntax mode = Theory.add_modesyntax mode o map Comment.ignore; -fun add_modesyntax_i mode = Theory.add_modesyntax_i mode o map Comment.ignore; -val add_trrules = Theory.add_trrules o map Comment.ignore; -val add_trrules_i = Theory.add_trrules_i o map Comment.ignore; -val add_judgment = ObjectLogic.add_judgment o Comment.ignore; -val add_judgment_i = ObjectLogic.add_judgment_i o Comment.ignore; - - (* axioms and defs *) fun add_axms f args thy = f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy; -val add_axioms = add_axms (#1 oo PureThy.add_axioms) o map Comment.ignore; -val add_axioms_i = (#1 oo PureThy.add_axioms_i) o map Comment.ignore; -fun add_defs (x, args) = add_axms (#1 oo PureThy.add_defs x) (map Comment.ignore args); -fun add_defs_i (x, args) = (#1 oo PureThy.add_defs_i x) (map Comment.ignore args); +val add_axioms = add_axms (#1 oo PureThy.add_axioms); +val add_axioms_i = #1 oo PureThy.add_axioms_i; +fun add_defs (x, args) = add_axms (#1 oo PureThy.add_defs x) args; +fun add_defs_i (x, args) = (#1 oo PureThy.add_defs_i x) args; (* constdefs *) fun gen_add_constdefs consts defs args thy = thy - |> consts (map (Comment.ignore o fst) args) - |> defs (false, map (fn (((c, _, mx), _), (s, _)) => - (((Thm.def_name (Syntax.const_name c mx), s), []), Comment.none)) args); + |> consts (map fst args) + |> defs (false, map (fn ((c, _, mx), s) => + ((Thm.def_name (Syntax.const_name c mx), s), [])) args); -fun add_constdefs args = gen_add_constdefs Theory.add_consts add_defs args; -fun add_constdefs_i args = gen_add_constdefs Theory.add_consts_i add_defs_i args; +val add_constdefs = gen_add_constdefs Theory.add_consts add_defs; +val add_constdefs_i = gen_add_constdefs Theory.add_consts_i add_defs_i; (* attributes *) @@ -355,30 +275,27 @@ in -fun theorems_i k = (present_thmss k oo PureThy.have_thmss_i (Drule.kind k)) o map Comment.ignore; -fun locale_theorems_i k loc = (present_thmss k oo Locale.have_thmss_i k loc) o map Comment.ignore; +fun theorems_i k = present_thmss k oo PureThy.have_thmss_i (Drule.kind k); +fun locale_theorems_i k loc = present_thmss k oo Locale.have_thmss_i k loc; fun theorems k args thy = thy - |> PureThy.have_thmss (Drule.kind k) (global_attribs thy (map Comment.ignore args)) + |> PureThy.have_thmss (Drule.kind k) (global_attribs thy args) |> present_thmss k; fun locale_theorems k loc args thy = thy - |> Locale.have_thmss k loc (local_attribs thy (map Comment.ignore args)) + |> Locale.have_thmss k loc (local_attribs thy args) |> present_thmss k; fun smart_theorems k opt_loc args thy = thy |> (case opt_loc of - None => PureThy.have_thmss (Drule.kind k) (global_attribs thy (map Comment.ignore args)) - | Some loc => Locale.have_thmss k loc (local_attribs thy (map Comment.ignore args))) + None => PureThy.have_thmss (Drule.kind k) (global_attribs thy args) + | Some loc => Locale.have_thmss k loc (local_attribs thy args)) |> present_thmss k; -fun declare_theorems opt_loc (args, comment) = - #1 o smart_theorems "" opt_loc [((("", []), args), comment)]; +fun declare_theorems opt_loc args = #1 o smart_theorems "" opt_loc [(("", []), args)]; -fun apply_theorems args = - apsnd (flat o map snd) o theorems "" [((("", []), args), Comment.none)]; -fun apply_theorems_i args = - apsnd (flat o map snd) o theorems_i "" [((("", []), args), Comment.none)]; +fun apply_theorems args = apsnd (flat o map snd) o theorems "" [(("", []), args)]; +fun apply_theorems_i args = apsnd (flat o map snd) o theorems_i "" [(("", []), args)]; end; @@ -391,25 +308,25 @@ fun chain_thmss f args = ProofHistory.apply (Proof.chain o f (map (pair ("", [])) args)); -val have_facts = ProofHistory.apply o local_thmss Proof.have_thmss o map Comment.ignore; -val have_facts_i = ProofHistory.apply o local_thmss_i Proof.have_thmss_i o map Comment.ignore; -val from_facts = chain_thmss (local_thmss Proof.have_thmss) o map Comment.ignore; -val from_facts_i = chain_thmss (local_thmss_i Proof.have_thmss_i) o map Comment.ignore; -val with_facts = chain_thmss (local_thmss Proof.with_thmss) o map Comment.ignore; -val with_facts_i = chain_thmss (local_thmss_i Proof.with_thmss_i) o map Comment.ignore; -fun chain comment_ignore = ProofHistory.apply Proof.chain; +val have_facts = ProofHistory.apply o local_thmss Proof.have_thmss; +val have_facts_i = ProofHistory.apply o local_thmss_i Proof.have_thmss_i; +val from_facts = chain_thmss (local_thmss Proof.have_thmss); +val from_facts_i = chain_thmss (local_thmss_i Proof.have_thmss_i); +val with_facts = chain_thmss (local_thmss Proof.with_thmss); +val with_facts_i = chain_thmss (local_thmss_i Proof.with_thmss_i); +val chain = ProofHistory.apply Proof.chain; (* context *) -val fix = ProofHistory.apply o Proof.fix o map Comment.ignore; -val fix_i = ProofHistory.apply o Proof.fix_i o map Comment.ignore; -val let_bind = ProofHistory.apply o Proof.let_bind o map Comment.ignore; -val let_bind_i = ProofHistory.apply o Proof.let_bind_i o map Comment.ignore; +val fix = ProofHistory.apply o Proof.fix; +val fix_i = ProofHistory.apply o Proof.fix_i; +val let_bind = ProofHistory.apply o Proof.let_bind; +val let_bind_i = ProofHistory.apply o Proof.let_bind_i; -fun invoke_case ((name, xs, src), comment_ignore) = ProofHistory.apply (fn state => +fun invoke_case (name, xs, src) = ProofHistory.apply (fn state => Proof.invoke_case (name, xs, map (Attrib.local_attribute (Proof.theory_of state)) src) state); -val invoke_case_i = ProofHistory.apply o Proof.invoke_case o Comment.ignore; +val invoke_case_i = ProofHistory.apply o Proof.invoke_case; (* local results *) @@ -487,94 +404,80 @@ fun multi_theorem k a elems args int thy = global_statement (Proof.multi_theorem k (apsnd (map (Attrib.global_attribute thy)) a) None - (map (Locale.attribute (Attrib.local_attribute thy)) elems)) (map Comment.ignore args) int thy; + (map (Locale.attribute (Attrib.local_attribute thy)) elems)) args int thy; -fun multi_theorem_i k a elems = - global_statement_i (Proof.multi_theorem_i k a None elems) o map Comment.ignore; +fun multi_theorem_i k a elems = global_statement_i (Proof.multi_theorem_i k a None elems); fun locale_multi_theorem k a locale elems args int thy = global_statement (Proof.multi_theorem k (apsnd (map (Attrib.global_attribute thy)) a) - (Some (locale, map (map (Attrib.local_attribute thy) o snd o fst o Comment.ignore) args)) + (Some (locale, map (map (Attrib.local_attribute thy) o snd o fst) args)) (map (Locale.attribute (Attrib.local_attribute thy)) elems)) - (map (apfst (apsnd (K [])) o Comment.ignore) args) int thy; + (map (apfst (apsnd (K []))) args) int thy; fun locale_multi_theorem_i k a locale elems args = - global_statement_i (Proof.multi_theorem_i k a - (Some (locale, map (snd o fst o Comment.ignore) args)) elems) - (map (apfst (apsnd (K [])) o Comment.ignore) args); + global_statement_i (Proof.multi_theorem_i k a (Some (locale, map (snd o fst) args)) elems) + (map (apfst (apsnd (K []))) args); -fun theorem k ((a, t), cmt) = multi_theorem k a [] [((("", []), [t]), cmt)]; -fun theorem_i k ((a, t), cmt) = multi_theorem_i k a [] [((("", []), [t]), cmt)]; +fun theorem k (a, t) = multi_theorem k a [] [(("", []), [t])]; +fun theorem_i k (a, t) = multi_theorem_i k a [] [(("", []), [t])]; fun smart_multi_theorem k a (None, elems) = multi_theorem k a elems | smart_multi_theorem k a (Some locale, elems) = locale_multi_theorem k a locale elems; -val assume = local_statement Proof.assume I o map Comment.ignore; -val assume_i = local_statement_i Proof.assume_i I o map Comment.ignore; -val presume = local_statement Proof.presume I o map Comment.ignore; -val presume_i = local_statement_i Proof.presume_i I o map Comment.ignore; -val have = local_statement (Proof.have Seq.single) I o map Comment.ignore; -val have_i = local_statement_i (Proof.have_i Seq.single) I o map Comment.ignore; -val hence = local_statement (Proof.have Seq.single) Proof.chain o map Comment.ignore; -val hence_i = local_statement_i (Proof.have_i Seq.single) Proof.chain o map Comment.ignore; -val show = local_statement' (Proof.show check_goal Seq.single) I o map Comment.ignore; -val show_i = local_statement_i' (Proof.show_i check_goal Seq.single) I o map Comment.ignore; -val thus = local_statement' (Proof.show check_goal Seq.single) Proof.chain o map Comment.ignore; -val thus_i = local_statement_i' (Proof.show_i check_goal Seq.single) Proof.chain o map Comment.ignore; +val assume = local_statement Proof.assume I; +val assume_i = local_statement_i Proof.assume_i I; +val presume = local_statement Proof.presume I; +val presume_i = local_statement_i Proof.presume_i I; +val have = local_statement (Proof.have Seq.single) I; +val have_i = local_statement_i (Proof.have_i Seq.single) I; +val hence = local_statement (Proof.have Seq.single) Proof.chain; +val hence_i = local_statement_i (Proof.have_i Seq.single) Proof.chain; +val show = local_statement' (Proof.show check_goal Seq.single) I; +val show_i = local_statement_i' (Proof.show_i check_goal Seq.single) I; +val thus = local_statement' (Proof.show check_goal Seq.single) Proof.chain; +val thus_i = local_statement_i' (Proof.show_i check_goal Seq.single) Proof.chain; fun gen_def f ((name, srcs), def) = ProofHistory.apply (fn state => f name (map (Attrib.local_attribute (Proof.theory_of state)) srcs) def state); -val local_def = gen_def Proof.def o Comment.ignore; -val local_def_i = gen_def Proof.def_i o Comment.ignore; +val local_def = gen_def Proof.def; +val local_def_i = gen_def Proof.def_i; fun obtain (xs, asms) = ProofHistory.applys (fn state => - Obtain.obtain (map Comment.ignore xs) - (map (local_attributes' state) (map Comment.ignore asms)) state); + Obtain.obtain xs (map (local_attributes' state) asms) state); -fun obtain_i (xs, asms) = ProofHistory.applys (fn state => - Obtain.obtain_i (map Comment.ignore xs) (map Comment.ignore asms) state); +fun obtain_i (xs, asms) = ProofHistory.applys (Obtain.obtain_i xs asms); end; (* blocks *) -fun begin_block comment_ignore = ProofHistory.apply Proof.begin_block; -fun next_block comment_ignore = ProofHistory.apply Proof.next_block; -fun end_block comment_ignore = ProofHistory.applys Proof.end_block; +val begin_block = ProofHistory.apply Proof.begin_block; +val next_block = ProofHistory.apply Proof.next_block; +val end_block = ProofHistory.applys Proof.end_block; (* shuffle state *) fun shuffle meth i = Method.refine (Method.Basic (K (meth i))) o Proof.assert_no_chain; -fun defer (i, comment_ignore) = ProofHistory.applys (shuffle Method.defer i); -fun prefer (i, comment_ignore) = ProofHistory.applys (shuffle Method.prefer i); +fun defer i = ProofHistory.applys (shuffle Method.defer i); +fun prefer i = ProofHistory.applys (shuffle Method.prefer i); (* backward steps *) -fun apply (m, comment_ignore) = ProofHistory.applys +fun apply m = ProofHistory.applys (Seq.map (Proof.goal_facts (K [])) o Method.refine m o Proof.assert_backward); - -fun apply_end (m, comment_ignore) = ProofHistory.applys - (Method.refine_end m o Proof.assert_forward); - -val proof = ProofHistory.applys o Method.proof o - apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore; +fun apply_end m = ProofHistory.applys (Method.refine_end m o Proof.assert_forward); +val proof = ProofHistory.applys o Method.proof; (* local endings *) -val local_qed = - proof'' o (ProofHistory.applys oo Method.local_qed true) o apsome Comment.ignore_interest; - -fun ignore_interests (x, y) = (Comment.ignore_interest x, apsome Comment.ignore_interest y); - -val local_terminal_proof = - proof'' o (ProofHistory.applys oo Method.local_terminal_proof) o ignore_interests; - +val local_qed = proof'' o (ProofHistory.applys oo Method.local_qed true); +val local_terminal_proof = proof'' o (ProofHistory.applys oo Method.local_terminal_proof); val local_default_proof = proof'' (ProofHistory.applys o Method.local_default_proof); val local_immediate_proof = proof'' (ProofHistory.applys o Method.local_immediate_proof); val local_done_proof = proof'' (ProofHistory.applys o Method.local_done_proof); @@ -596,9 +499,8 @@ thy end); -fun global_qed m = global_result (K (Method.global_qed true (apsome Comment.ignore_interest m))); -fun global_terminal_proof m = - global_result (K (Method.global_terminal_proof (ignore_interests m))); +fun global_qed m = global_result (K (Method.global_qed true m)); +fun global_terminal_proof m = global_result (K (Method.global_terminal_proof m)); val global_default_proof = global_result (K Method.global_default_proof); val global_immediate_proof = global_result (K Method.global_immediate_proof); val global_skip_proof = global_result SkipProof.global_skip_proof; @@ -607,14 +509,13 @@ (* common endings *) -fun qed (meth, comment) = local_qed meth o global_qed meth; -fun terminal_proof (meths, comment) = local_terminal_proof meths o global_terminal_proof meths; -fun default_proof comment = local_default_proof o global_default_proof; -fun immediate_proof comment = local_immediate_proof o global_immediate_proof; -fun done_proof comment = local_done_proof o global_done_proof; -fun skip_proof comment = local_skip_proof o global_skip_proof; - -fun forget_proof comment = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current); +fun qed meth = local_qed meth o global_qed meth; +fun terminal_proof meths = local_terminal_proof meths o global_terminal_proof meths; +val default_proof = local_default_proof o global_default_proof; +val immediate_proof = local_immediate_proof o global_immediate_proof; +val done_proof = local_done_proof o global_done_proof; +val skip_proof = local_skip_proof o global_skip_proof; +val forget_proof = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current); (* calculational proof commands *) @@ -628,8 +529,8 @@ fun proof''' f = Toplevel.proof' (f o cond_print_calc); -fun gen_calc get f (args, _) prt state = - f (apsome (fn (srcs, _) => get srcs state) args) prt state; +fun gen_calc get f args prt state = + f (apsome (fn srcs => get srcs state) args) prt state; in @@ -640,8 +541,8 @@ fun also_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.also x); fun finally x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.finally x); fun finally_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.finally x); -fun moreover comment = proof''' (ProofHistory.apply o Calculation.moreover); -fun ultimately comment = proof''' (ProofHistory.apply o Calculation.ultimately); +val moreover = proof''' (ProofHistory.apply o Calculation.moreover); +val ultimately = proof''' (ProofHistory.apply o Calculation.ultimately); end; @@ -650,32 +551,32 @@ val parse_ast_translation = Context.use_let "val parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list" - "Theory.add_trfuns (parse_ast_translation, [], [], [])" o Comment.ignore; + "Theory.add_trfuns (parse_ast_translation, [], [], [])"; val parse_translation = Context.use_let "val parse_translation: (string * (term list -> term)) list" - "Theory.add_trfuns ([], parse_translation, [], [])" o Comment.ignore; + "Theory.add_trfuns ([], parse_translation, [], [])"; val print_translation = Context.use_let "val print_translation: (string * (term list -> term)) list" - "Theory.add_trfuns ([], [], print_translation, [])" o Comment.ignore; + "Theory.add_trfuns ([], [], print_translation, [])"; val print_ast_translation = Context.use_let "val print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list" - "Theory.add_trfuns ([], [], [], print_ast_translation)" o Comment.ignore; + "Theory.add_trfuns ([], [], [], print_ast_translation)"; val typed_print_translation = Context.use_let "val typed_print_translation: (string * (bool -> typ -> term list -> term)) list" - "Theory.add_trfunsT typed_print_translation" o Comment.ignore; + "Theory.add_trfunsT typed_print_translation"; val token_translation = Context.use_let "val token_translation: (string * string * (string -> string * real)) list" - "Theory.add_tokentrfuns token_translation" o Comment.ignore; + "Theory.add_tokentrfuns token_translation"; (* add method *) -fun method_setup ((name, txt, cmt), comment_ignore) = +fun method_setup (name, txt, cmt) = Context.use_let "val thm = PureThy.get_thm_closure (Context.the_context ());\n\ \val thms = PureThy.get_thms_closure (Context.the_context ());\n\ @@ -686,7 +587,7 @@ (* add_oracle *) -fun add_oracle ((name, txt), comment_ignore) = +fun add_oracle (name, txt) = Context.use_let "val oracle: bstring * (Sign.sg * Object.T -> term)" "Theory.add_oracle oracle" @@ -696,8 +597,7 @@ (* add_locale *) fun add_locale (name, import, body) thy = - Locale.add_locale name import - (map (Locale.attribute (Attrib.local_attribute thy) o Comment.ignore) body) thy; + Locale.add_locale name import (map (Locale.attribute (Attrib.local_attribute thy)) body) thy; (* theory init and exit *) diff -r bda60442bf02 -r a70df1e5bf10 src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/Pure/Isar/outer_parse.ML Tue Feb 12 20:28:27 2002 +0100 @@ -45,9 +45,6 @@ val xname: token list -> xstring * token list val text: token list -> string * token list val uname: token list -> string option * token list - val comment: token list -> Comment.text * token list - val marg_comment: token list -> Comment.text * token list - val interest: token list -> Comment.interest * token list val sort: token list -> string * token list val arity: token list -> (string list * string) * token list val simple_arity: token list -> (string list * xclass) * token list @@ -177,15 +174,6 @@ val uname = underscore >> K None || name >> Some; -(* formal comments *) - -val comment = text >> (Comment.plain o Library.single); -val marg_comment = Scan.repeat ($$$ "--" |-- text) >> Comment.plain; - -val interest = Scan.optional ($$$ "%%" >> K Comment.no_interest || - $$$ "%" |-- Scan.optional nat 1 >> Comment.interest) Comment.default_interest; - - (* sorts and arities *) val sort = group "sort" xname; diff -r bda60442bf02 -r a70df1e5bf10 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Tue Feb 12 20:28:27 2002 +0100 @@ -228,20 +228,19 @@ (* basic sources *) -fun token_source (src, pos) = - src - |> Symbol.source false - |> T.source false (K (get_lexicons ())) pos; - fun toplevel_source term do_recover cmd src = let val no_terminator = Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof)); - val recover = Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [None]; + fun recover x = (Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [None]) x; in src + |> T.source_proper |> Source.source T.stopper - (Scan.bulk (fn xs => P.!!! (command term (cmd ())) xs)) + (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K None || P.not_eof >> Some)) + (if do_recover then Some recover else None) + |> Source.mapfilter I + |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term (cmd ())) xs)) (if do_recover then Some recover else None) |> Source.mapfilter I end; @@ -254,7 +253,6 @@ |> Symbol.source true |> T.source true get_lexicons (if no_pos then Position.none else Position.line_name 1 "stdin") - |> T.source_proper |> toplevel_source term true get_parser; @@ -294,7 +292,6 @@ fun parse_thy src = src - |> T.source_proper |> toplevel_source false false (K (get_parser ())) |> Source.exhaust; @@ -311,7 +308,10 @@ Present.old_symbol_source name present_text) (*note: text presented twice*) else let - val tok_src = Source.exhausted (token_source (text_src, pos)); + val tok_src = text_src + |> Symbol.source false + |> T.source false (K (get_lexicons ())) pos + |> Source.exhausted; val out = Toplevel.excursion_result (IsarOutput.parse_thy markup (#1 (get_lexicons ())) (parse_thy tok_src) tok_src); diff -r bda60442bf02 -r a70df1e5bf10 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/Pure/axclass.ML Tue Feb 12 20:28:27 2002 +0100 @@ -26,12 +26,10 @@ val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory val default_intro_classes_tac: thm list -> int -> tactic val axclass_tac: thm list -> tactic - val instance_subclass_proof: (xclass * xclass) * Comment.text -> bool -> theory -> ProofHistory.T - val instance_subclass_proof_i: (class * class) * Comment.text -> bool -> theory -> ProofHistory.T - val instance_arity_proof: (xstring * string list * xclass) * Comment.text - -> bool -> theory -> ProofHistory.T - val instance_arity_proof_i: (string * sort list * class) * Comment.text - -> bool -> theory -> ProofHistory.T + val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T + val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T + val instance_arity_proof: xstring * string list * xclass -> bool -> theory -> ProofHistory.T + val instance_arity_proof_i: string * sort list * class -> bool -> theory -> ProofHistory.T val setup: (theory -> theory) list end; @@ -421,10 +419,10 @@ fun inst_attribute add_thms (thy, thm) = (add_thms [thm] thy, thm); -fun inst_proof mk_prop add_thms (sig_prop, comment) int thy = +fun inst_proof mk_prop add_thms sig_prop int thy = thy - |> IsarThy.theorem_i Drule.internalK ((("", [inst_attribute add_thms]), - (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int; + |> IsarThy.theorem_i Drule.internalK (("", [inst_attribute add_thms]), + (mk_prop (Theory.sign_of thy) sig_prop, ([], []))) int; val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms; val instance_subclass_proof_i = inst_proof (mk_classrel oo cert_classrel) add_classrel_thms; @@ -448,17 +446,14 @@ val axclassP = OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl - (((P.name -- Scan.optional ((P.$$$ "\\" || P.$$$ "<") |-- - P.!!! (P.list1 P.xname)) []) --| P.marg_comment) - -- Scan.repeat (P.spec_name --| P.marg_comment) + ((P.name -- Scan.optional ((P.$$$ "\\" || P.$$$ "<") |-- + P.!!! (P.list1 P.xname)) []) -- Scan.repeat P.spec_name >> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs))); val instanceP = OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal - ((P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.xname) - -- P.marg_comment >> instance_subclass_proof || - (P.xname -- (P.$$$ "::" |-- P.simple_arity) >> P.triple2) -- P.marg_comment - >> instance_arity_proof) + ((P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.xname) >> instance_subclass_proof || + (P.xname -- (P.$$$ "::" |-- P.simple_arity) >> P.triple2) >> instance_arity_proof) >> (Toplevel.print oo Toplevel.theory_to_proof)); val _ = OuterSyntax.add_parsers [axclassP, instanceP]; diff -r bda60442bf02 -r a70df1e5bf10 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/ZF/Tools/datatype_package.ML Tue Feb 12 20:28:27 2002 +0100 @@ -419,14 +419,14 @@ val con_decl = P.name -- Scan.optional (P.$$$ "(" |-- P.list1 P.term --| P.$$$ ")") [] -- P.opt_mixfix - --| P.marg_comment >> P.triple1; + >> P.triple1; val datatype_decl = - (Scan.optional ((P.$$$ "\\" || P.$$$ "<=") |-- P.!!! P.term --| P.marg_comment) "") -- + (Scan.optional ((P.$$$ "\\" || P.$$$ "<=") |-- P.!!! P.term) "") -- P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) -- - Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] -- - Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1 --| P.marg_comment) [] -- - Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1 --| P.marg_comment) [] + Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] -- + Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1) [] -- + Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1) [] >> (Toplevel.theory o mk_datatype); val coind_prefix = if coind then "co" else ""; diff -r bda60442bf02 -r a70df1e5bf10 src/ZF/Tools/ind_cases.ML --- a/src/ZF/Tools/ind_cases.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/ZF/Tools/ind_cases.ML Tue Feb 12 20:28:27 2002 +0100 @@ -55,8 +55,8 @@ val read_prop = ProofContext.read_prop (ProofContext.init thy); val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop; val facts = args |> map (fn ((name, srcs), props) => - (((name, map (Attrib.global_attribute thy) srcs), - map (Thm.no_attributes o single o mk_cases) props), Comment.none)); + ((name, map (Attrib.global_attribute thy) srcs), + map (Thm.no_attributes o single o mk_cases) props)); in thy |> IsarThy.theorems_i Drule.lemmaK facts |> #1 end; @@ -84,7 +84,7 @@ local structure P = OuterParse and K = OuterSyntax.Keyword in val ind_cases = - P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop --| P.marg_comment) + P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop) >> (Toplevel.theory o inductive_cases); val inductive_casesP = diff -r bda60442bf02 -r a70df1e5bf10 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/ZF/Tools/inductive_package.ML Tue Feb 12 20:28:27 2002 +0100 @@ -605,13 +605,13 @@ val ind_decl = (P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term -- - ((P.$$$ "\\" || P.$$$ "<=") |-- P.term)) --| P.marg_comment) -- + ((P.$$$ "\\" || P.$$$ "<=") |-- P.term))) -- (P.$$$ "intros" |-- - P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) -- - Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] -- - Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) [] -- - Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1 --| P.marg_comment) [] -- - Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1 --| P.marg_comment) [] + P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) -- + Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] -- + Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1) [] -- + Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1) [] -- + Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1) [] >> (Toplevel.theory o mk_ind); val inductiveP = OuterSyntax.command (co_prefix ^ "inductive") diff -r bda60442bf02 -r a70df1e5bf10 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Tue Feb 12 20:25:58 2002 +0100 +++ b/src/ZF/Tools/primrec_package.ML Tue Feb 12 20:28:27 2002 +0100 @@ -202,7 +202,7 @@ local structure P = OuterParse and K = OuterSyntax.Keyword in -val primrec_decl = Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment); +val primrec_decl = Scan.repeat1 (P.opt_thm_name ":" -- P.prop); val primrecP = OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl