wneuper/isa: src/Pure/Isar/isar

     1 (*  Title:      Pure/Isar/isar_syn.ML

     2     Author:     Markus Wenzel, TU Muenchen

     4 Isar/Pure outer syntax.

     5 *)

     7 structure Isar_Syn: sig end =

     8 struct

    10 (** keywords **)

    12 val _ = Context.>> (Context.map_theory

    13   (fold (fn name => (Keyword.define (name, NONE); Thy_Header.declare_keyword (name, NONE)))

    14    ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",

    15     "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",

    16     "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",

    17     "advanced", "and", "assumes", "attach", "begin", "binder",

    18     "constrains", "defines", "fixes", "for", "identifier", "if",

    19     "imports", "in", "infix", "infixl", "infixr", "is", "keywords",

    20     "notes", "obtains", "open", "output", "overloaded", "pervasive",

    21     "shows", "structure", "unchecked", "uses", "where", "|"]));

    25 (** init and exit **)

    27 val _ =

    28   Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory"

    29     (Thy_Header.args >> (fn header =>

    30       Toplevel.print o

    31         Toplevel.init_theory

    32           (fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));

    34 val _ =

    35   Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end (local) theory"

    36     (Scan.succeed

    37       (Toplevel.exit o Toplevel.end_local_theory o Toplevel.end_proof (K Proof.end_notepad)));

    41 (** markup commands **)

    43 val _ =

    44   Outer_Syntax.markup_command Thy_Output.Markup

    45     ("header", Keyword.diag) "theory header"

    46     (Parse.doc_source >> Isar_Cmd.header_markup);

    48 val _ =

    49   Outer_Syntax.markup_command Thy_Output.Markup

    50     ("chapter", Keyword.thy_heading1) "chapter heading"

    51     (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);

    53 val _ =

    54   Outer_Syntax.markup_command Thy_Output.Markup

    55     ("section", Keyword.thy_heading2) "section heading"

    56     (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);

    58 val _ =

    59   Outer_Syntax.markup_command Thy_Output.Markup

    60     ("subsection", Keyword.thy_heading3) "subsection heading"

    61     (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);

    63 val _ =

    64   Outer_Syntax.markup_command Thy_Output.Markup

    65     ("subsubsection", Keyword.thy_heading4) "subsubsection heading"

    66     (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);

    68 val _ =

    69   Outer_Syntax.markup_command Thy_Output.MarkupEnv

    70     ("text", Keyword.thy_decl) "formal comment (theory)"

    71     (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);

    73 val _ =

    74   Outer_Syntax.markup_command Thy_Output.Verbatim

    75     ("text_raw", Keyword.thy_decl) "raw document preparation text"

    76     (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);

    78 val _ =

    79   Outer_Syntax.markup_command Thy_Output.Markup

    80     ("sect", Keyword.tag_proof Keyword.prf_heading2) "formal comment (proof)"

    81     (Parse.doc_source >> Isar_Cmd.proof_markup);

    83 val _ =

    84   Outer_Syntax.markup_command Thy_Output.Markup

    85     ("subsect", Keyword.tag_proof Keyword.prf_heading3) "formal comment (proof)"

    86     (Parse.doc_source >> Isar_Cmd.proof_markup);

    88 val _ =

    89   Outer_Syntax.markup_command Thy_Output.Markup

    90     ("subsubsect", Keyword.tag_proof Keyword.prf_heading4) "formal comment (proof)"

    91     (Parse.doc_source >> Isar_Cmd.proof_markup);

    93 val _ =

    94   Outer_Syntax.markup_command Thy_Output.MarkupEnv

    95     ("txt", Keyword.tag_proof Keyword.prf_decl) "formal comment (proof)"

    96     (Parse.doc_source >> Isar_Cmd.proof_markup);

    98 val _ =

    99   Outer_Syntax.markup_command Thy_Output.Verbatim

   100     ("txt_raw", Keyword.tag_proof Keyword.prf_decl) "raw document preparation text (proof)"

   101     (Parse.doc_source >> Isar_Cmd.proof_markup);

   105 (** theory commands **)

   107 (* classes and sorts *)

   109 val _ =

   110   Outer_Syntax.command ("classes", Keyword.thy_decl) "declare type classes"

   111     (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |--

   112         Parse.!!! (Parse.list1 Parse.class)) [])

   113       >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));

   115 val _ =

   116   Outer_Syntax.command ("classrel", Keyword.thy_decl) "state inclusion of type classes (axiomatic!)"

   117     (Parse.and_list1 (Parse.class -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")

   118         |-- Parse.!!! Parse.class))

   119     >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));

   121 val _ =

   122   Outer_Syntax.local_theory ("default_sort", Keyword.thy_decl)

   123     "declare default sort for explicit type variables"

   124     (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));

   127 (* types *)

   129 val _ =

   130   Outer_Syntax.local_theory ("typedecl", Keyword.thy_decl) "type declaration"

   131     (Parse.type_args -- Parse.binding -- Parse.opt_mixfix

   132       >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));

   134 val _ =

   135   Outer_Syntax.local_theory ("type_synonym", Keyword.thy_decl) "declare type abbreviation"

   136     (Parse.type_args -- Parse.binding --

   137       (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))

   138       >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));

   140 val _ =

   141   Outer_Syntax.command ("nonterminal", Keyword.thy_decl)

   142     "declare syntactic type constructors (grammar nonterminal symbols)"

   143     (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));

   145 val _ =

   146   Outer_Syntax.command ("arities", Keyword.thy_decl) "state type arities (axiomatic!)"

   147     (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));

   150 (* consts and syntax *)

   152 val _ =

   153   Outer_Syntax.command ("judgment", Keyword.thy_decl) "declare object-logic judgment"

   154     (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));

   156 val _ =

   157   Outer_Syntax.command ("consts", Keyword.thy_decl) "declare constants"

   158     (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));

   160 val opt_overloaded = Parse.opt_keyword "overloaded";

   162 val mode_spec =

   163   (Parse.$$$ "output" >> K ("", false)) ||

   164     Parse.name -- Scan.optional (Parse.$$$ "output" >> K false) true;

   166 val opt_mode =

   167   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (mode_spec --| Parse.$$$ ")")) Syntax.mode_default;

   169 val _ =

   170   Outer_Syntax.command ("syntax", Keyword.thy_decl) "declare syntactic constants"

   171     (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax));

   173 val _ =

   174   Outer_Syntax.command ("no_syntax", Keyword.thy_decl) "delete syntax declarations"

   175     (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax));

   178 (* translations *)

   180 val trans_pat =

   181   Scan.optional

   182     (Parse.$$$ "(" |-- Parse.!!! (Parse.xname --| Parse.$$$ ")")) "logic"

   183     -- Parse.inner_syntax Parse.string;

   185 fun trans_arrow toks =

   186   ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.Parse_Rule ||

   187     (Parse.$$$ "\\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.Print_Rule ||

   188     (Parse.$$$ "\\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.Parse_Print_Rule) toks;

   190 val trans_line =

   191   trans_pat -- Parse.!!! (trans_arrow -- trans_pat)

   192     >> (fn (left, (arr, right)) => arr (left, right));

   194 val _ =

   195   Outer_Syntax.command ("translations", Keyword.thy_decl) "declare syntax translation rules"

   196     (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));

   198 val _ =

   199   Outer_Syntax.command ("no_translations", Keyword.thy_decl) "remove syntax translation rules"

   200     (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));

   203 (* axioms and definitions *)

   205 val _ =

   206   Outer_Syntax.command ("axioms", Keyword.thy_decl) "state arbitrary propositions (axiomatic!)"

   207     (Scan.repeat1 Parse_Spec.spec >>

   208       (fn spec => Toplevel.theory (fn thy =>

   209         (legacy_feature "Old 'axioms' command -- use 'axiomatization' instead";

   210           Isar_Cmd.add_axioms spec thy))));

   212 val opt_unchecked_overloaded =

   213   Scan.optional (Parse.$$$ "(" |-- Parse.!!!

   214     (((Parse.$$$ "unchecked" >> K true) -- Scan.optional (Parse.$$$ "overloaded" >> K true) false ||

   215       Parse.$$$ "overloaded" >> K (false, true)) --| Parse.$$$ ")")) (false, false);

   217 val _ =

   218   Outer_Syntax.command ("defs", Keyword.thy_decl) "define constants"

   219     (opt_unchecked_overloaded --

   220       Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))

   221       >> (Toplevel.theory o Isar_Cmd.add_defs));

   224 (* constant definitions and abbreviations *)

   226 val _ =

   227   Outer_Syntax.local_theory' ("definition", Keyword.thy_decl) "constant definition"

   228     (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));

   230 val _ =

   231   Outer_Syntax.local_theory' ("abbreviation", Keyword.thy_decl) "constant abbreviation"

   232     (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)

   233       >> (fn (mode, args) => Specification.abbreviation_cmd mode args));

   235 val _ =

   236   Outer_Syntax.local_theory ("type_notation", Keyword.thy_decl)

   237     "add concrete syntax for type constructors"

   238     (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)

   239       >> (fn (mode, args) => Specification.type_notation_cmd true mode args));

   241 val _ =

   242   Outer_Syntax.local_theory ("no_type_notation", Keyword.thy_decl)

   243     "delete concrete syntax for type constructors"

   244     (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)

   245       >> (fn (mode, args) => Specification.type_notation_cmd false mode args));

   247 val _ =

   248   Outer_Syntax.local_theory ("notation", Keyword.thy_decl)

   249     "add concrete syntax for constants / fixed variables"

   250     (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)

   251       >> (fn (mode, args) => Specification.notation_cmd true mode args));

   253 val _ =

   254   Outer_Syntax.local_theory ("no_notation", Keyword.thy_decl)

   255     "delete concrete syntax for constants / fixed variables"

   256     (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)

   257       >> (fn (mode, args) => Specification.notation_cmd false mode args));

   260 (* constant specifications *)

   262 val _ =

   263   Outer_Syntax.command ("axiomatization", Keyword.thy_decl) "axiomatic constant specification"

   264     (Scan.optional Parse.fixes [] --

   265       Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []

   266       >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));

   269 (* theorems *)

   271 fun theorems kind =

   272   Parse_Spec.name_facts -- Parse.for_fixes

   273     >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd kind facts fixes);

   275 val _ =

   276   Outer_Syntax.local_theory' ("theorems", Keyword.thy_decl) "define theorems"

   277     (theorems Thm.theoremK);

   279 val _ =

   280   Outer_Syntax.local_theory' ("lemmas", Keyword.thy_decl) "define lemmas" (theorems Thm.lemmaK);

   282 val _ =

   283   Outer_Syntax.local_theory' ("declare", Keyword.thy_decl) "declare theorems"

   284     (Parse.and_list1 Parse_Spec.xthms1 -- Parse.for_fixes

   285       >> (fn (facts, fixes) =>

   286           #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));

   289 (* name space entry path *)

   291 fun hide_names name hide what =

   292   Outer_Syntax.command (name, Keyword.thy_decl) ("hide " ^ what ^ " from name space")

   293     ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>

   294       (Toplevel.theory o uncurry hide));

   296 val _ = hide_names "hide_class" Isar_Cmd.hide_class "classes";

   297 val _ = hide_names "hide_type" Isar_Cmd.hide_type "types";

   298 val _ = hide_names "hide_const" Isar_Cmd.hide_const "constants";

   299 val _ = hide_names "hide_fact" Isar_Cmd.hide_fact "facts";

   302 (* use ML text *)

   304 val _ =

   305   Outer_Syntax.command ("use", Keyword.tag_ml Keyword.thy_decl) "ML text from file"

   306     (Parse.path >> (fn path => Toplevel.generic_theory (Thy_Load.exec_ml path)));

   308 val _ =

   309   Outer_Syntax.command ("ML", Keyword.tag_ml Keyword.thy_decl)

   310     "ML text within theory or local theory"

   311     (Parse.ML_source >> (fn (txt, pos) =>

   312       Toplevel.generic_theory

   313         (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>

   314           Local_Theory.propagate_ml_env)));

   316 val _ =

   317   Outer_Syntax.command ("ML_prf", Keyword.tag_proof Keyword.prf_decl) "ML text within proof"

   318     (Parse.ML_source >> (fn (txt, pos) =>

   319       Toplevel.proof (Proof.map_context (Context.proof_map

   320         (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));

   322 val _ =

   323   Outer_Syntax.command ("ML_val", Keyword.tag_ml Keyword.diag) "diagnostic ML text"

   324     (Parse.ML_source >> Isar_Cmd.ml_diag true);

   326 val _ =

   327   Outer_Syntax.command ("ML_command", Keyword.tag_ml Keyword.diag) "diagnostic ML text (silent)"

   328     (Parse.ML_source >> (Toplevel.no_timing oo Isar_Cmd.ml_diag false));

   330 val _ =

   331   Outer_Syntax.command ("setup", Keyword.tag_ml Keyword.thy_decl) "ML theory setup"

   332     (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup));

   334 val _ =

   335   Outer_Syntax.local_theory ("local_setup", Keyword.tag_ml Keyword.thy_decl) "ML local theory setup"

   336     (Parse.ML_source >> Isar_Cmd.local_setup);

   338 val _ =

   339   Outer_Syntax.command ("attribute_setup", Keyword.tag_ml Keyword.thy_decl) "define attribute in ML"

   340     (Parse.position Parse.name --

   341         Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Scan.optional Parse.text "")

   342       >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));

   344 val _ =

   345   Outer_Syntax.command ("method_setup", Keyword.tag_ml Keyword.thy_decl) "define proof method in ML"

   346     (Parse.position Parse.name --

   347         Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Scan.optional Parse.text "")

   348       >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));

   350 val _ =

   351   Outer_Syntax.local_theory ("declaration", Keyword.tag_ml Keyword.thy_decl)

   352     "generic ML declaration"

   353     (Parse.opt_keyword "pervasive" -- Parse.ML_source

   354       >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));

   356 val _ =

   357   Outer_Syntax.local_theory ("syntax_declaration", Keyword.tag_ml Keyword.thy_decl)

   358     "generic ML declaration"

   359     (Parse.opt_keyword "pervasive" -- Parse.ML_source

   360       >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));

   362 val _ =

   363   Outer_Syntax.local_theory ("simproc_setup", Keyword.tag_ml Keyword.thy_decl)

   364     "define simproc in ML"

   365     (Parse.position Parse.name --

   366       (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --

   367       Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []

   368     >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));

   371 (* translation functions *)

   373 val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;

   375 val _ =

   376   Outer_Syntax.command ("parse_ast_translation", Keyword.tag_ml Keyword.thy_decl)

   377     "install parse ast translation functions"

   378     (trfun >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));

   380 val _ =

   381   Outer_Syntax.command ("parse_translation", Keyword.tag_ml Keyword.thy_decl)

   382     "install parse translation functions"

   383     (trfun >> (Toplevel.theory o Isar_Cmd.parse_translation));

   385 val _ =

   386   Outer_Syntax.command ("print_translation", Keyword.tag_ml Keyword.thy_decl)

   387     "install print translation functions"

   388     (trfun >> (Toplevel.theory o Isar_Cmd.print_translation));

   390 val _ =

   391   Outer_Syntax.command ("typed_print_translation", Keyword.tag_ml Keyword.thy_decl)

   392     "install typed print translation functions"

   393     (trfun >> (Toplevel.theory o Isar_Cmd.typed_print_translation));

   395 val _ =

   396   Outer_Syntax.command ("print_ast_translation", Keyword.tag_ml Keyword.thy_decl)

   397     "install print ast translation functions"

   398     (trfun >> (Toplevel.theory o Isar_Cmd.print_ast_translation));

   401 (* oracles *)

   403 val _ =

   404   Outer_Syntax.command ("oracle", Keyword.tag_ml Keyword.thy_decl) "declare oracle"

   405     (Parse.position Parse.name -- (Parse.$$$ "=" |-- Parse.ML_source) >>

   406       (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));

   409 (* local theories *)

   411 val _ =

   412   Outer_Syntax.command ("context", Keyword.thy_decl) "enter local theory context"

   413     (Parse.position Parse.xname --| Parse.begin >> (fn name =>

   414       Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));

   417 (* locales *)

   419 val locale_val =

   420   Parse_Spec.locale_expression false --

   421     Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||

   422   Scan.repeat1 Parse_Spec.context_element >> pair ([], []);

   424 val _ =

   425   Outer_Syntax.command ("locale", Keyword.thy_decl) "define named proof context"

   426     (Parse.binding --

   427       Scan.optional (Parse.$$$ "=" |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin

   428       >> (fn ((name, (expr, elems)), begin) =>

   429           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin

   430             (Expression.add_locale_cmd I name Binding.empty expr elems #> snd)));

   432 fun parse_interpretation_arguments mandatory =

   433   Parse.!!! (Parse_Spec.locale_expression mandatory) --

   434     Scan.optional

   435       (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];

   437 val _ =

   438   Outer_Syntax.command ("sublocale", Keyword.thy_goal)

   439     "prove sublocale relation between a locale and a locale expression"

   440     (Parse.position Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --

   441       parse_interpretation_arguments false

   442       >> (fn (loc, (expr, equations)) =>

   443           Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));

   445 val _ =

   446   Outer_Syntax.command ("interpretation", Keyword.thy_goal)

   447     "prove interpretation of locale expression in theory"

   448     (parse_interpretation_arguments true

   449       >> (fn (expr, equations) => Toplevel.print o

   450           Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));

   452 val _ =

   453   Outer_Syntax.command ("interpret", Keyword.tag_proof Keyword.prf_goal)

   454     "prove interpretation of locale expression in proof context"

   455     (parse_interpretation_arguments true

   456       >> (fn (expr, equations) => Toplevel.print o

   457           Toplevel.proof' (Expression.interpret_cmd expr equations)));

   460 (* classes *)

   462 val class_val =

   463   Parse_Spec.class_expression --

   464     Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||

   465   Scan.repeat1 Parse_Spec.context_element >> pair [];

   467 val _ =

   468   Outer_Syntax.command ("class", Keyword.thy_decl) "define type class"

   469    (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin

   470     >> (fn ((name, (supclasses, elems)), begin) =>

   471         (begin ? Toplevel.print) o Toplevel.begin_local_theory begin

   472           (Class_Declaration.class_cmd I name supclasses elems #> snd)));

   474 val _ =

   475   Outer_Syntax.local_theory_to_proof ("subclass", Keyword.thy_goal) "prove a subclass relation"

   476     (Parse.class >> Class_Declaration.subclass_cmd I);

   478 val _ =

   479   Outer_Syntax.command ("instantiation", Keyword.thy_decl) "instantiate and prove type arity"

   480    (Parse.multi_arity --| Parse.begin

   481      >> (fn arities => Toplevel.print o

   482          Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));

   484 val _ =

   485   Outer_Syntax.command ("instance", Keyword.thy_goal) "prove type arity or subclass relation"

   486   ((Parse.class --

   487     ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||

   488     Parse.multi_arity >> Class.instance_arity_cmd)

   489     >> (Toplevel.print oo Toplevel.theory_to_proof) ||

   490     Scan.succeed

   491       (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));

   494 (* arbitrary overloading *)

   496 val _ =

   497   Outer_Syntax.command ("overloading", Keyword.thy_decl) "overloaded definitions"

   498    (Scan.repeat1 (Parse.name --| (Parse.$$$ "\\<equiv>" || Parse.$$$ "==") -- Parse.term --

   499       Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true

   500       >> Parse.triple1) --| Parse.begin

   501    >> (fn operations => Toplevel.print o

   502          Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));

   505 (* code generation *)

   507 val _ =

   508   Outer_Syntax.command ("code_datatype", Keyword.thy_decl)

   509     "define set of code datatype constructors"

   510     (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));

   514 (** proof commands **)

   516 (* statements *)

   518 fun gen_theorem schematic kind =

   519   Outer_Syntax.local_theory_to_proof'

   520     (if schematic then ("schematic_" ^ kind, Keyword.thy_schematic_goal)

   521      else (kind, Keyword.thy_goal))

   522     ("state " ^ (if schematic then "schematic " ^ kind else kind))

   523     (Scan.optional (Parse_Spec.opt_thm_name ":" --|

   524       Scan.ahead (Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --

   525       Parse_Spec.general_statement >> (fn (a, (elems, concl)) =>

   526         ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)

   527           kind NONE (K I) a elems concl)));

   529 val _ = gen_theorem false Thm.theoremK;

   530 val _ = gen_theorem false Thm.lemmaK;

   531 val _ = gen_theorem false Thm.corollaryK;

   532 val _ = gen_theorem true Thm.theoremK;

   533 val _ = gen_theorem true Thm.lemmaK;

   534 val _ = gen_theorem true Thm.corollaryK;

   536 val _ =

   537   Outer_Syntax.local_theory_to_proof ("notepad", Keyword.thy_decl)

   538     "Isar proof state as formal notepad, without any result"

   539     (Parse.begin >> K Proof.begin_notepad);

   541 val _ =

   542   Outer_Syntax.command ("have", Keyword.tag_proof Keyword.prf_goal) "state local goal"

   543     (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));

   545 val _ =

   546   Outer_Syntax.command ("hence", Keyword.tag_proof Keyword.prf_goal) "abbreviates \"then have\""

   547     (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));

   549 val _ =

   550   Outer_Syntax.command ("show", Keyword.tag_proof Keyword.prf_asm_goal)

   551     "state local goal, solving current obligation"

   552     (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));

   554 val _ =

   555   Outer_Syntax.command ("thus", Keyword.tag_proof Keyword.prf_asm_goal) "abbreviates \"then show\""

   556     (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));

   559 (* facts *)

   561 val facts = Parse.and_list1 Parse_Spec.xthms1;

   563 val _ =

   564   Outer_Syntax.command ("then", Keyword.tag_proof Keyword.prf_chain) "forward chaining"

   565     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));

   567 val _ =

   568   Outer_Syntax.command ("from", Keyword.tag_proof Keyword.prf_chain)

   569     "forward chaining from given facts"

   570     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));

   572 val _ =

   573   Outer_Syntax.command ("with", Keyword.tag_proof Keyword.prf_chain)

   574     "forward chaining from given and current facts"

   575     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));

   577 val _ =

   578   Outer_Syntax.command ("note", Keyword.tag_proof Keyword.prf_decl) "define facts"

   579     (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));

   581 val _ =

   582   Outer_Syntax.command ("using", Keyword.tag_proof Keyword.prf_decl) "augment goal facts"

   583     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));

   585 val _ =

   586   Outer_Syntax.command ("unfolding", Keyword.tag_proof Keyword.prf_decl)

   587     "unfold definitions in goal and facts"

   588     (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));

   591 (* proof context *)

   593 val _ =

   594   Outer_Syntax.command ("fix", Keyword.tag_proof Keyword.prf_asm)

   595     "fix local variables (Skolem constants)"

   596     (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));

   598 val _ =

   599   Outer_Syntax.command ("assume", Keyword.tag_proof Keyword.prf_asm) "assume propositions"

   600     (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));

   602 val _ =

   603   Outer_Syntax.command ("presume", Keyword.tag_proof Keyword.prf_asm)

   604     "assume propositions, to be established later"

   605     (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));

   607 val _ =

   608   Outer_Syntax.command ("def", Keyword.tag_proof Keyword.prf_asm) "local definition"

   609     (Parse.and_list1

   610       (Parse_Spec.opt_thm_name ":" --

   611         ((Parse.binding -- Parse.opt_mixfix) --

   612           ((Parse.$$$ "\\<equiv>" || Parse.$$$ "==") |-- Parse.!!! Parse.termp)))

   613     >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));

   615 val _ =

   616   Outer_Syntax.command ("obtain", Keyword.tag_proof Keyword.prf_asm_goal)

   617     "generalized elimination"

   618     (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement

   619       >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));

   621 val _ =

   622   Outer_Syntax.command ("guess", Keyword.tag_proof Keyword.prf_asm_goal)

   623     "wild guessing (unstructured)"

   624     (Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));

   626 val _ =

   627   Outer_Syntax.command ("let", Keyword.tag_proof Keyword.prf_decl) "bind text variables"

   628     (Parse.and_list1 (Parse.and_list1 Parse.term -- (Parse.$$$ "=" |-- Parse.term))

   629       >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));

   631 val _ =

   632   Outer_Syntax.command ("write", Keyword.tag_proof Keyword.prf_decl)

   633     "add concrete syntax for constants / fixed variables"

   634     (opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)

   635     >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));

   637 val case_spec =

   638   (Parse.$$$ "(" |--

   639     Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.binding) --| Parse.$$$ ")") ||

   640     Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1;

   642 val _ =

   643   Outer_Syntax.command ("case", Keyword.tag_proof Keyword.prf_asm) "invoke local context"

   644     (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));

   647 (* proof structure *)

   649 val _ =

   650   Outer_Syntax.command ("{", Keyword.tag_proof Keyword.prf_open) "begin explicit proof block"

   651     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));

   653 val _ =

   654   Outer_Syntax.command ("}", Keyword.tag_proof Keyword.prf_close) "end explicit proof block"

   655     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));

   657 val _ =

   658   Outer_Syntax.command ("next", Keyword.tag_proof Keyword.prf_block) "enter next proof block"

   659     (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));

   662 (* end proof *)

   664 val _ =

   665   Outer_Syntax.command ("qed", Keyword.tag_proof Keyword.qed_block) "conclude (sub-)proof"

   666     (Scan.option Method.parse >> Isar_Cmd.qed);

   668 val _ =

   669   Outer_Syntax.command ("by", Keyword.tag_proof Keyword.qed) "terminal backward proof"

   670     (Method.parse -- Scan.option Method.parse >> Isar_Cmd.terminal_proof);

   672 val _ =

   673   Outer_Syntax.command ("..", Keyword.tag_proof Keyword.qed) "default proof"

   674     (Scan.succeed Isar_Cmd.default_proof);

   676 val _ =

   677   Outer_Syntax.command (".", Keyword.tag_proof Keyword.qed) "immediate proof"

   678     (Scan.succeed Isar_Cmd.immediate_proof);

   680 val _ =

   681   Outer_Syntax.command ("done", Keyword.tag_proof Keyword.qed) "done proof"

   682     (Scan.succeed Isar_Cmd.done_proof);

   684 val _ =

   685   Outer_Syntax.command ("sorry", Keyword.tag_proof Keyword.qed)

   686     "skip proof (quick-and-dirty mode only!)"

   687     (Scan.succeed Isar_Cmd.skip_proof);

   689 val _ =

   690   Outer_Syntax.command ("oops", Keyword.tag_proof Keyword.qed_global) "forget proof"

   691     (Scan.succeed Toplevel.forget_proof);

   694 (* proof steps *)

   696 val _ =

   697   Outer_Syntax.command ("defer", Keyword.tag_proof Keyword.prf_script)

   698     "shuffle internal proof state"

   699     (Scan.option Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));

   701 val _ =

   702   Outer_Syntax.command ("prefer", Keyword.tag_proof Keyword.prf_script)

   703     "shuffle internal proof state"

   704     (Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));

   706 val _ =

   707   Outer_Syntax.command ("apply", Keyword.tag_proof Keyword.prf_script)

   708     "initial refinement step (unstructured)"

   709     (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));

   711 val _ =

   712   Outer_Syntax.command ("apply_end", Keyword.tag_proof Keyword.prf_script)

   713     "terminal refinement (unstructured)"

   714     (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));

   716 val _ =

   717   Outer_Syntax.command ("proof", Keyword.tag_proof Keyword.prf_block) "backward proof"

   718     (Scan.option Method.parse >> (fn m => Toplevel.print o

   719       Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o

   720       Toplevel.skip_proof (fn i => i + 1)));

   723 (* calculational proof commands *)

   725 val calc_args =

   726   Scan.option (Parse.$$$ "(" |-- Parse.!!! ((Parse_Spec.xthms1 --| Parse.$$$ ")")));

   728 val _ =

   729   Outer_Syntax.command ("also", Keyword.tag_proof Keyword.prf_decl)

   730     "combine calculation and current facts"

   731     (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));

   733 val _ =

   734   Outer_Syntax.command ("finally", Keyword.tag_proof Keyword.prf_chain)

   735     "combine calculation and current facts, exhibit result"

   736     (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));

   738 val _ =

   739   Outer_Syntax.command ("moreover", Keyword.tag_proof Keyword.prf_decl)

   740     "augment calculation by current facts"

   741     (Scan.succeed (Toplevel.proof' Calculation.moreover));

   743 val _ =

   744   Outer_Syntax.command ("ultimately", Keyword.tag_proof Keyword.prf_chain)

   745     "augment calculation by current facts, exhibit result"

   746     (Scan.succeed (Toplevel.proof' Calculation.ultimately));

   749 (* proof navigation *)

   751 val _ =

   752   Outer_Syntax.command ("back", Keyword.tag_proof Keyword.prf_script)

   753     "backtracking of proof command"

   754     (Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I));

   757 (* nested commands *)

   759 val props_text =

   760   Scan.optional Parse.properties [] -- Parse.position Parse.string

   761   >> (fn (props, (str, pos)) =>

   762       (Position.of_properties (Position.default_properties pos props), str));

   764 val _ =

   765   Outer_Syntax.improper_command ("Isabelle.command", Keyword.control) "nested Isabelle command"

   766     (props_text :|-- (fn (pos, str) =>

   767       (case Outer_Syntax.parse pos str of

   768         [tr] => Scan.succeed (K tr)

   769       | _ => Scan.fail_with (K (fn () => "exactly one command expected")))

   770       handle ERROR msg => Scan.fail_with (K (fn () => msg))));

   774 (** diagnostic commands (for interactive mode only) **)

   776 val opt_modes =

   777   Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];

   779 val opt_bang = Scan.optional (Parse.$$$ "!" >> K true) false;

   781 val _ =

   782   Outer_Syntax.improper_command ("pretty_setmargin", Keyword.diag)

   783     "change default margin for pretty printing"

   784     (Parse.nat >>

   785       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Pretty.margin_default := n)));

   787 val _ =

   788   Outer_Syntax.improper_command ("help", Keyword.diag) "print outer syntax commands"

   789     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));

   791 val _ =

   792   Outer_Syntax.improper_command ("print_commands", Keyword.diag) "print outer syntax commands"

   793     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));

   795 val _ =

   796   Outer_Syntax.improper_command ("print_configs", Keyword.diag) "print configuration options"

   797     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_configs));

   799 val _ =

   800   Outer_Syntax.improper_command ("print_context", Keyword.diag) "print theory context name"

   801     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_context));

   803 val _ =

   804   Outer_Syntax.improper_command ("print_theory", Keyword.diag)

   805     "print logical theory contents (verbose!)"

   806     (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theory));

   808 val _ =

   809   Outer_Syntax.improper_command ("print_syntax", Keyword.diag)

   810     "print inner syntax of context (verbose!)"

   811     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_syntax));

   813 val _ =

   814   Outer_Syntax.improper_command ("print_abbrevs", Keyword.diag)

   815     "print constant abbreviation of context"

   816     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_abbrevs));

   818 val _ =

   819   Outer_Syntax.improper_command ("print_theorems", Keyword.diag)

   820     "print theorems of local theory or proof context"

   821     (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theorems));

   823 val _ =

   824   Outer_Syntax.improper_command ("print_locales", Keyword.diag)

   825     "print locales of this theory"

   826     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_locales));

   828 val _ =

   829   Outer_Syntax.improper_command ("print_classes", Keyword.diag) "print classes of this theory"

   830     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o

   831       Toplevel.keep (Class.print_classes o Toplevel.context_of)));

   833 val _ =

   834   Outer_Syntax.improper_command ("print_locale", Keyword.diag) "print locale of this theory"

   835     (opt_bang -- Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));

   837 val _ =

   838   Outer_Syntax.improper_command ("print_interps", Keyword.diag)

   839     "print interpretations of locale for this theory or proof context"

   840     (Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));

   842 val _ =

   843   Outer_Syntax.improper_command ("print_dependencies", Keyword.diag)

   844     "print dependencies of locale expression"

   845     (opt_bang -- Parse_Spec.locale_expression true >>

   846       (Toplevel.no_timing oo Isar_Cmd.print_dependencies));

   848 val _ =

   849   Outer_Syntax.improper_command ("print_attributes", Keyword.diag)

   850     "print attributes of this theory"

   851     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes));

   853 val _ =

   854   Outer_Syntax.improper_command ("print_simpset", Keyword.diag)

   855     "print context of Simplifier"

   856     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_simpset));

   858 val _ =

   859   Outer_Syntax.improper_command ("print_rules", Keyword.diag) "print intro/elim rules"

   860     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_rules));

   862 val _ =

   863   Outer_Syntax.improper_command ("print_trans_rules", Keyword.diag) "print transitivity rules"

   864     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_trans_rules));

   866 val _ =

   867   Outer_Syntax.improper_command ("print_methods", Keyword.diag) "print methods of this theory"

   868     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_methods));

   870 val _ =

   871   Outer_Syntax.improper_command ("print_antiquotations", Keyword.diag)

   872     "print antiquotations (global)"

   873     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_antiquotations));

   875 val _ =

   876   Outer_Syntax.improper_command ("thy_deps", Keyword.diag) "visualize theory dependencies"

   877     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));

   879 val _ =

   880   Outer_Syntax.improper_command ("class_deps", Keyword.diag) "visualize class dependencies"

   881     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));

   883 val _ =

   884   Outer_Syntax.improper_command ("thm_deps", Keyword.diag) "visualize theorem dependencies"

   885     (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));

   887 val _ =

   888   Outer_Syntax.improper_command ("print_binds", Keyword.diag) "print term bindings of proof context"

   889     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_binds));

   891 val _ =

   892   Outer_Syntax.improper_command ("print_facts", Keyword.diag) "print facts of proof context"

   893     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_facts));

   895 val _ =

   896   Outer_Syntax.improper_command ("print_cases", Keyword.diag) "print cases of proof context"

   897     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_cases));

   899 val _ =

   900   Outer_Syntax.improper_command ("print_statement", Keyword.diag)

   901     "print theorems as long statements"

   902     (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_stmts));

   904 val _ =

   905   Outer_Syntax.improper_command ("thm", Keyword.diag) "print theorems"

   906     (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_thms));

   908 val _ =

   909   Outer_Syntax.improper_command ("prf", Keyword.diag) "print proof terms of theorems"

   910     (opt_modes -- Scan.option Parse_Spec.xthms1

   911       >> (Toplevel.no_timing oo Isar_Cmd.print_prfs false));

   913 val _ =

   914   Outer_Syntax.improper_command ("full_prf", Keyword.diag) "print full proof terms of theorems"

   915     (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_prfs true));

   917 val _ =

   918   Outer_Syntax.improper_command ("prop", Keyword.diag) "read and print proposition"

   919     (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_prop));

   921 val _ =

   922   Outer_Syntax.improper_command ("term", Keyword.diag) "read and print term"

   923     (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_term));

   925 val _ =

   926   Outer_Syntax.improper_command ("typ", Keyword.diag) "read and print type"

   927     (opt_modes -- Parse.typ >> (Toplevel.no_timing oo Isar_Cmd.print_type));

   929 val _ =

   930   Outer_Syntax.improper_command ("print_codesetup", Keyword.diag) "print code generator setup"

   931     (Scan.succeed

   932       (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep

   933         (Code.print_codesetup o Toplevel.theory_of)));

   935 val _ =

   936   Outer_Syntax.improper_command ("unused_thms", Keyword.diag) "find unused theorems"

   937     (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --

   938        Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>

   939          (Toplevel.no_timing oo Isar_Cmd.unused_thms));

   943 (** system commands (for interactive mode only) **)

   945 val _ =

   946   Outer_Syntax.improper_command ("cd", Keyword.control) "change current working directory"

   947     (Parse.path >> (fn path => Toplevel.no_timing o Toplevel.imperative (fn () => File.cd path)));

   949 val _ =

   950   Outer_Syntax.improper_command ("pwd", Keyword.diag) "print current working directory"

   951     (Scan.succeed (Toplevel.no_timing o

   952       Toplevel.imperative (fn () => writeln (Path.print (File.pwd ())))));

   954 val _ =

   955   Outer_Syntax.improper_command ("use_thy", Keyword.control) "use theory file"

   956     (Parse.name >> (fn name =>

   957       Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));

   959 val _ =

   960   Outer_Syntax.improper_command ("remove_thy", Keyword.control) "remove theory from loader database"

   961     (Parse.name >> (fn name =>

   962       Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.remove_thy name)));

   964 val _ =

   965   Outer_Syntax.improper_command ("kill_thy", Keyword.control)

   966     "kill theory -- try to remove from loader database"

   967     (Parse.name >> (fn name =>

   968       Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.kill_thy name)));

   970 val _ =

   971   Outer_Syntax.improper_command ("display_drafts", Keyword.diag)

   972     "display raw source files with symbols"

   973     (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));

   975 val _ =

   976   Outer_Syntax.improper_command ("print_drafts", Keyword.diag)

   977     "print raw source files with symbols"

   978     (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));

   980 val _ =  (* FIXME tty only *)

   981   Outer_Syntax.improper_command ("pr", Keyword.diag) "print current proof state (if present)"

   982     (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>

   983       Toplevel.no_timing o Toplevel.keep (fn state =>

   984        (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n;

   985         Toplevel.quiet := false;

   986         Print_Mode.with_modes modes (Toplevel.print_state true) state))));

   988 val _ =

   989   Outer_Syntax.improper_command ("disable_pr", Keyword.control)

   990     "disable printing of toplevel state"

   991     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := true)));

   993 val _ =

   994   Outer_Syntax.improper_command ("enable_pr", Keyword.control)

   995     "enable printing of toplevel state"

   996     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := false)));

   998 val _ =

   999   Outer_Syntax.improper_command ("commit", Keyword.control)

  1000     "commit current session to ML database"

  1001     (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));

  1003 val _ =

  1004   Outer_Syntax.improper_command ("quit", Keyword.control) "quit Isabelle"

  1005     (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative quit)));

  1007 val _ =

  1008   Outer_Syntax.improper_command ("exit", Keyword.control) "exit Isar loop"

  1009     (Scan.succeed

  1010       (Toplevel.no_timing o Toplevel.keep (fn state =>

  1011         (Context.set_thread_data (try Toplevel.generic_theory_of state);

  1012           raise Runtime.TERMINATE))));

  1014 end;

author	wenzelm
	Sat, 17 Mar 2012 22:46:19 +0100
changeset 47870	1c3c185bab4e
parent 47845	7ca3608146d8
child 47928	12423b36fcc4
permissions	-rw-r--r--