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 (*keep keywords consistent with the parsers, otherwise be prepared for

    13   unexpected errors*)

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

    16   (fold (fn name => Thy_Header.declare_keyword (name, NONE))

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

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

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

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

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

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

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

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

    28 (** init and exit **)

    30 val _ =

    31   Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)

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

    33       Toplevel.print o

    34         Toplevel.init_theory

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

    37 val _ =

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

    39     (Scan.succeed

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

    44 (** markup commands **)

    46 val _ = Outer_Syntax.markup_command Thy_Output.Markup "header" "theory header" Keyword.diag

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

    49 val _ = Outer_Syntax.markup_command Thy_Output.Markup "chapter" "chapter heading"

    50   Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);

    52 val _ = Outer_Syntax.markup_command Thy_Output.Markup "section" "section heading"

    53   Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);

    55 val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsection" "subsection heading"

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

    58 val _ =

    59   Outer_Syntax.markup_command Thy_Output.Markup "subsubsection" "subsubsection heading"

    60   Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);

    62 val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "text" "formal comment (theory)"

    63   Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);

    65 val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "text_raw" "raw document preparation text"

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

    68 val _ = Outer_Syntax.markup_command Thy_Output.Markup "sect" "formal comment (proof)"

    69   (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);

    71 val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsect" "formal comment (proof)"

    72   (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);

    74 val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsubsect" "formal comment (proof)"

    75   (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);

    77 val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "txt" "formal comment (proof)"

    78   (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> Isar_Cmd.proof_markup);

    80 val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "txt_raw"

    81   "raw document preparation text (proof)" (Keyword.tag_proof Keyword.prf_decl)

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

    86 (** theory commands **)

    88 (* classes and sorts *)

    90 val _ =

    91   Outer_Syntax.command "classes" "declare type classes" Keyword.thy_decl

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

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

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

    96 val _ =

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

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

    99         |-- Parse.!!! Parse.class))

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

   102 val _ =

   103   Outer_Syntax.local_theory "default_sort" "declare default sort for explicit type variables"

   104     Keyword.thy_decl

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

   108 (* types *)

   110 val _ =

   111   Outer_Syntax.local_theory "typedecl" "type declaration" Keyword.thy_decl

   112     (Parse.type_args -- Parse.binding -- Parse.opt_mixfix

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

   115 val _ =

   116   Outer_Syntax.local_theory "type_synonym" "declare type abbreviation" Keyword.thy_decl

   117     (Parse.type_args -- Parse.binding --

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

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

   121 val _ =

   122   Outer_Syntax.command "nonterminal"

   123     "declare syntactic type constructors (grammar nonterminal symbols)" Keyword.thy_decl

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

   126 val _ =

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

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

   131 (* consts and syntax *)

   133 val _ =

   134   Outer_Syntax.command "judgment" "declare object-logic judgment" Keyword.thy_decl

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

   137 val _ =

   138   Outer_Syntax.command "consts" "declare constants" Keyword.thy_decl

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

   141 val opt_overloaded = Parse.opt_keyword "overloaded";

   143 val _ =

   144   Outer_Syntax.command "finalconsts" "declare constants as final" Keyword.thy_decl

   145     (opt_overloaded -- Scan.repeat1 Parse.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));

   147 val mode_spec =

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

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

   151 val opt_mode =

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

   154 val _ =

   155   Outer_Syntax.command "syntax" "declare syntactic constants" Keyword.thy_decl

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

   158 val _ =

   159   Outer_Syntax.command "no_syntax" "delete syntax declarations" Keyword.thy_decl

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

   163 (* translations *)

   165 val trans_pat =

   166   Scan.optional

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

   168     -- Parse.inner_syntax Parse.string;

   170 fun trans_arrow toks =

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

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

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

   175 val trans_line =

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

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

   179 val _ =

   180   Outer_Syntax.command "translations" "declare syntax translation rules" Keyword.thy_decl

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

   183 val _ =

   184   Outer_Syntax.command "no_translations" "remove syntax translation rules" Keyword.thy_decl

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

   188 (* axioms and definitions *)

   190 val _ =

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

   192     (Scan.repeat1 Parse_Spec.spec >>

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

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

   195           Isar_Cmd.add_axioms spec thy))));

   197 val opt_unchecked_overloaded =

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

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

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

   202 val _ =

   203   Outer_Syntax.command "defs" "define constants" Keyword.thy_decl

   204     (opt_unchecked_overloaded --

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

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

   209 (* constant definitions and abbreviations *)

   211 val _ =

   212   Outer_Syntax.local_theory' "definition" "constant definition" Keyword.thy_decl

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

   215 val _ =

   216   Outer_Syntax.local_theory' "abbreviation" "constant abbreviation" Keyword.thy_decl

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

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

   220 val _ =

   221   Outer_Syntax.local_theory "type_notation" "add concrete syntax for type constructors"

   222     Keyword.thy_decl

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

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

   226 val _ =

   227   Outer_Syntax.local_theory "no_type_notation" "delete concrete syntax for type constructors"

   228     Keyword.thy_decl

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

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

   232 val _ =

   233   Outer_Syntax.local_theory "notation" "add concrete syntax for constants / fixed variables"

   234     Keyword.thy_decl

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

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

   238 val _ =

   239   Outer_Syntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables"

   240     Keyword.thy_decl

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

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

   245 (* constant specifications *)

   247 val _ =

   248   Outer_Syntax.command "axiomatization" "axiomatic constant specification" Keyword.thy_decl

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

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

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

   254 (* theorems *)

   256 fun theorems kind =

   257   Parse_Spec.name_facts -- Parse.for_fixes

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

   260 val _ =

   261   Outer_Syntax.local_theory' "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);

   263 val _ =

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

   266 val _ =

   267   Outer_Syntax.local_theory' "declare" "declare theorems" Keyword.thy_decl

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

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

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

   273 (* name space entry path *)

   275 fun hide_names name hide what =

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

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

   278       (Toplevel.theory o uncurry hide));

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

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

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

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

   286 (* use ML text *)

   288 val _ =

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

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

   292 val _ =

   293   Outer_Syntax.command "ML" "ML text within theory or local theory"

   294     (Keyword.tag_ml Keyword.thy_decl)

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

   296       Toplevel.generic_theory

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

   298           Local_Theory.propagate_ml_env)));

   300 val _ =

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

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

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

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

   306 val _ =

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

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

   310 val _ =

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

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

   314 val _ =

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

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

   318 val _ =

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

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

   322 val _ =

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

   324     (Parse.position Parse.name --

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

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

   328 val _ =

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

   330     (Parse.position Parse.name --

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

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

   334 val _ =

   335   Outer_Syntax.local_theory "declaration" "generic ML declaration"

   336     (Keyword.tag_ml Keyword.thy_decl)

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

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

   340 val _ =

   341   Outer_Syntax.local_theory "syntax_declaration" "generic ML declaration"

   342     (Keyword.tag_ml Keyword.thy_decl)

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

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

   346 val _ =

   347   Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)

   348     (Parse.position Parse.name --

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

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

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

   354 (* translation functions *)

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

   358 val _ =

   359   Outer_Syntax.command "parse_ast_translation" "install parse ast translation functions"

   360     (Keyword.tag_ml Keyword.thy_decl)

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

   363 val _ =

   364   Outer_Syntax.command "parse_translation" "install parse translation functions"

   365     (Keyword.tag_ml Keyword.thy_decl)

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

   368 val _ =

   369   Outer_Syntax.command "print_translation" "install print translation functions"

   370     (Keyword.tag_ml Keyword.thy_decl)

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

   373 val _ =

   374   Outer_Syntax.command "typed_print_translation" "install typed print translation functions"

   375     (Keyword.tag_ml Keyword.thy_decl)

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

   378 val _ =

   379   Outer_Syntax.command "print_ast_translation" "install print ast translation functions"

   380     (Keyword.tag_ml Keyword.thy_decl)

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

   384 (* oracles *)

   386 val _ =

   387   Outer_Syntax.command "oracle" "declare oracle" (Keyword.tag_ml Keyword.thy_decl)

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

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

   392 (* local theories *)

   394 val _ =

   395   Outer_Syntax.command "context" "enter local theory context" Keyword.thy_decl

   396     (Parse.position Parse.name --| Parse.begin >> (fn name =>

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

   400 (* locales *)

   402 val locale_val =

   403   Parse_Spec.locale_expression false --

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

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

   407 val _ =

   408   Outer_Syntax.command "locale" "define named proof context" Keyword.thy_decl

   409     (Parse.binding --

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

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

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

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

   415 fun parse_interpretation_arguments mandatory =

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

   417     Scan.optional

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

   420 val _ =

   421   Outer_Syntax.command "sublocale"

   422     "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal

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

   424       parse_interpretation_arguments false

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

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

   428 val _ =

   429   Outer_Syntax.command "interpretation"

   430     "prove interpretation of locale expression in theory" Keyword.thy_goal

   431     (parse_interpretation_arguments true

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

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

   435 val _ =

   436   Outer_Syntax.command "interpret"

   437     "prove interpretation of locale expression in proof context"

   438     (Keyword.tag_proof Keyword.prf_goal)

   439     (parse_interpretation_arguments true

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

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

   444 (* classes *)

   446 val class_val =

   447   Parse_Spec.class_expression --

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

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

   451 val _ =

   452   Outer_Syntax.command "class" "define type class" Keyword.thy_decl

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

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

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

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

   458 val _ =

   459   Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal

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

   462 val _ =

   463   Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl

   464    (Parse.multi_arity --| Parse.begin

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

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

   468 val _ =

   469   Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal

   470   ((Parse.class --

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

   472     Parse.multi_arity >> Class.instance_arity_cmd)

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

   474     Scan.succeed

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

   478 (* arbitrary overloading *)

   480 val _ =

   481   Outer_Syntax.command "overloading" "overloaded definitions" Keyword.thy_decl

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

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

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

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

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

   489 (* code generation *)

   491 val _ =

   492   Outer_Syntax.command "code_datatype" "define set of code datatype constructors" Keyword.thy_decl

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

   497 (** proof commands **)

   499 (* statements *)

   501 fun gen_theorem schematic kind =

   502   Outer_Syntax.local_theory_to_proof'

   503     (if schematic then "schematic_" ^ kind else kind)

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

   505     (if schematic then Keyword.thy_schematic_goal else Keyword.thy_goal)

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

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

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

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

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

   512 val _ = gen_theorem false Thm.theoremK;

   513 val _ = gen_theorem false Thm.lemmaK;

   514 val _ = gen_theorem false Thm.corollaryK;

   515 val _ = gen_theorem true Thm.theoremK;

   516 val _ = gen_theorem true Thm.lemmaK;

   517 val _ = gen_theorem true Thm.corollaryK;

   519 val _ =

   520   Outer_Syntax.local_theory_to_proof "notepad"

   521     "Isar proof state as formal notepad, without any result" Keyword.thy_decl

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

   524 val _ =

   525   Outer_Syntax.command "have" "state local goal"

   526     (Keyword.tag_proof Keyword.prf_goal)

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

   529 val _ =

   530   Outer_Syntax.command "hence" "abbreviates \"then have\""

   531     (Keyword.tag_proof Keyword.prf_goal)

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

   534 val _ =

   535   Outer_Syntax.command "show" "state local goal, solving current obligation"

   536     (Keyword.tag_proof Keyword.prf_asm_goal)

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

   539 val _ =

   540   Outer_Syntax.command "thus" "abbreviates \"then show\""

   541     (Keyword.tag_proof Keyword.prf_asm_goal)

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

   545 (* facts *)

   547 val facts = Parse.and_list1 Parse_Spec.xthms1;

   549 val _ =

   550   Outer_Syntax.command "then" "forward chaining"

   551     (Keyword.tag_proof Keyword.prf_chain)

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

   554 val _ =

   555   Outer_Syntax.command "from" "forward chaining from given facts"

   556     (Keyword.tag_proof Keyword.prf_chain)

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

   559 val _ =

   560   Outer_Syntax.command "with" "forward chaining from given and current facts"

   561     (Keyword.tag_proof Keyword.prf_chain)

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

   564 val _ =

   565   Outer_Syntax.command "note" "define facts"

   566     (Keyword.tag_proof Keyword.prf_decl)

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

   569 val _ =

   570   Outer_Syntax.command "using" "augment goal facts"

   571     (Keyword.tag_proof Keyword.prf_decl)

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

   574 val _ =

   575   Outer_Syntax.command "unfolding" "unfold definitions in goal and facts"

   576     (Keyword.tag_proof Keyword.prf_decl)

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

   580 (* proof context *)

   582 val _ =

   583   Outer_Syntax.command "fix" "fix local variables (Skolem constants)"

   584     (Keyword.tag_proof Keyword.prf_asm)

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

   587 val _ =

   588   Outer_Syntax.command "assume" "assume propositions"

   589     (Keyword.tag_proof Keyword.prf_asm)

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

   592 val _ =

   593   Outer_Syntax.command "presume" "assume propositions, to be established later"

   594     (Keyword.tag_proof Keyword.prf_asm)

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

   597 val _ =

   598   Outer_Syntax.command "def" "local definition"

   599     (Keyword.tag_proof Keyword.prf_asm)

   600     (Parse.and_list1

   601       (Parse_Spec.opt_thm_name ":" --

   602         ((Parse.binding -- Parse.opt_mixfix) --

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

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

   606 val _ =

   607   Outer_Syntax.command "obtain" "generalized existence"

   608     (Keyword.tag_proof Keyword.prf_asm_goal)

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

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

   612 val _ =

   613   Outer_Syntax.command "guess" "wild guessing (unstructured)"

   614     (Keyword.tag_proof Keyword.prf_asm_goal)

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

   617 val _ =

   618   Outer_Syntax.command "let" "bind text variables"

   619     (Keyword.tag_proof Keyword.prf_decl)

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

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

   623 val _ =

   624   Outer_Syntax.command "write" "add concrete syntax for constants / fixed variables"

   625     (Keyword.tag_proof Keyword.prf_decl)

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

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

   629 val case_spec =

   630   (Parse.$$$ "(" |--

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

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

   634 val _ =

   635   Outer_Syntax.command "case" "invoke local context"

   636     (Keyword.tag_proof Keyword.prf_asm)

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

   640 (* proof structure *)

   642 val _ =

   643   Outer_Syntax.command "{" "begin explicit proof block"

   644     (Keyword.tag_proof Keyword.prf_open)

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

   647 val _ =

   648   Outer_Syntax.command "}" "end explicit proof block"

   649     (Keyword.tag_proof Keyword.prf_close)

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

   652 val _ =

   653   Outer_Syntax.command "next" "enter next proof block"

   654     (Keyword.tag_proof Keyword.prf_block)

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

   658 (* end proof *)

   660 val _ =

   661   Outer_Syntax.command "qed" "conclude (sub-)proof"

   662     (Keyword.tag_proof Keyword.qed_block)

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

   665 val _ =

   666   Outer_Syntax.command "by" "terminal backward proof"

   667     (Keyword.tag_proof Keyword.qed)

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

   670 val _ =

   671   Outer_Syntax.command ".." "default proof"

   672     (Keyword.tag_proof Keyword.qed)

   673     (Scan.succeed Isar_Cmd.default_proof);

   675 val _ =

   676   Outer_Syntax.command "." "immediate proof"

   677     (Keyword.tag_proof Keyword.qed)

   678     (Scan.succeed Isar_Cmd.immediate_proof);

   680 val _ =

   681   Outer_Syntax.command "done" "done proof"

   682     (Keyword.tag_proof Keyword.qed)

   683     (Scan.succeed Isar_Cmd.done_proof);

   685 val _ =

   686   Outer_Syntax.command "sorry" "skip proof (quick-and-dirty mode only!)"

   687     (Keyword.tag_proof Keyword.qed)

   688     (Scan.succeed Isar_Cmd.skip_proof);

   690 val _ =

   691   Outer_Syntax.command "oops" "forget proof"

   692     (Keyword.tag_proof Keyword.qed_global)

   693     (Scan.succeed Toplevel.forget_proof);

   696 (* proof steps *)

   698 val _ =

   699   Outer_Syntax.command "defer" "shuffle internal proof state"

   700     (Keyword.tag_proof Keyword.prf_script)

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

   703 val _ =

   704   Outer_Syntax.command "prefer" "shuffle internal proof state"

   705     (Keyword.tag_proof Keyword.prf_script)

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

   708 val _ =

   709   Outer_Syntax.command "apply" "initial refinement step (unstructured)"

   710     (Keyword.tag_proof Keyword.prf_script)

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

   713 val _ =

   714   Outer_Syntax.command "apply_end" "terminal refinement (unstructured)"

   715     (Keyword.tag_proof Keyword.prf_script)

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

   718 val _ =

   719   Outer_Syntax.command "proof" "backward proof"

   720     (Keyword.tag_proof Keyword.prf_block)

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

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

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

   726 (* calculational proof commands *)

   728 val calc_args =

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

   731 val _ =

   732   Outer_Syntax.command "also" "combine calculation and current facts"

   733     (Keyword.tag_proof Keyword.prf_decl)

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

   736 val _ =

   737   Outer_Syntax.command "finally" "combine calculation and current facts, exhibit result"

   738     (Keyword.tag_proof Keyword.prf_chain)

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

   741 val _ =

   742   Outer_Syntax.command "moreover" "augment calculation by current facts"

   743     (Keyword.tag_proof Keyword.prf_decl)

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

   746 val _ =

   747   Outer_Syntax.command "ultimately" "augment calculation by current facts, exhibit result"

   748     (Keyword.tag_proof Keyword.prf_chain)

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

   752 (* proof navigation *)

   754 val _ =

   755   Outer_Syntax.command "back" "backtracking of proof command"

   756     (Keyword.tag_proof Keyword.prf_script)

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

   760 (* nested commands *)

   762 val props_text =

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

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

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

   767 val _ =

   768   Outer_Syntax.improper_command "Isabelle.command" "nested Isabelle command" Keyword.control

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

   770       (case Outer_Syntax.parse pos str of

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

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

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

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

   779 val opt_modes =

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

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

   784 val _ =

   785   Outer_Syntax.improper_command "pretty_setmargin" "change default margin for pretty printing"

   786     Keyword.diag (Parse.nat >>

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

   789 val _ =

   790   Outer_Syntax.improper_command "help" "print outer syntax commands" Keyword.diag

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

   793 val _ =

   794   Outer_Syntax.improper_command "print_commands" "print outer syntax commands" Keyword.diag

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

   797 val _ =

   798   Outer_Syntax.improper_command "print_configs" "print configuration options" Keyword.diag

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

   801 val _ =

   802   Outer_Syntax.improper_command "print_context" "print theory context name" Keyword.diag

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

   805 val _ =

   806   Outer_Syntax.improper_command "print_theory" "print logical theory contents (verbose!)"

   807     Keyword.diag (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theory));

   809 val _ =

   810   Outer_Syntax.improper_command "print_syntax" "print inner syntax of context (verbose!)"

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

   813 val _ =

   814   Outer_Syntax.improper_command "print_abbrevs" "print constant abbreviation of context"

   815     Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_abbrevs));

   817 val _ =

   818   Outer_Syntax.improper_command "print_theorems"

   819       "print theorems of local theory or proof context" Keyword.diag

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

   822 val _ =

   823   Outer_Syntax.improper_command "print_locales" "print locales of this theory" Keyword.diag

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

   826 val _ =

   827   Outer_Syntax.improper_command "print_classes" "print classes of this theory" Keyword.diag

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

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

   831 val _ =

   832   Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag

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

   835 val _ =

   836   Outer_Syntax.improper_command "print_interps"

   837     "print interpretations of locale for this theory or proof context" Keyword.diag

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

   840 val _ =

   841   Outer_Syntax.improper_command "print_dependencies"

   842     "print dependencies of locale expression" Keyword.diag

   843     (opt_bang -- Parse_Spec.locale_expression true >>

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

   846 val _ =

   847   Outer_Syntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag

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

   850 val _ =

   851   Outer_Syntax.improper_command "print_simpset" "print context of Simplifier" Keyword.diag

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

   854 val _ =

   855   Outer_Syntax.improper_command "print_rules" "print intro/elim rules" Keyword.diag

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

   858 val _ =

   859   Outer_Syntax.improper_command "print_trans_rules" "print transitivity rules" Keyword.diag

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

   862 val _ =

   863   Outer_Syntax.improper_command "print_methods" "print methods of this theory" Keyword.diag

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

   866 val _ =

   867   Outer_Syntax.improper_command "print_antiquotations" "print antiquotations (global)" Keyword.diag

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

   870 val _ =

   871   Outer_Syntax.improper_command "thy_deps" "visualize theory dependencies"

   872     Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));

   874 val _ =

   875   Outer_Syntax.improper_command "class_deps" "visualize class dependencies"

   876     Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));

   878 val _ =

   879   Outer_Syntax.improper_command "thm_deps" "visualize theorem dependencies"

   880     Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));

   882 val _ =

   883   Outer_Syntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag

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

   886 val _ =

   887   Outer_Syntax.improper_command "print_facts" "print facts of proof context" Keyword.diag

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

   890 val _ =

   891   Outer_Syntax.improper_command "print_cases" "print cases of proof context" Keyword.diag

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

   894 val _ =

   895   Outer_Syntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag

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

   898 val _ =

   899   Outer_Syntax.improper_command "thm" "print theorems" Keyword.diag

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

   902 val _ =

   903   Outer_Syntax.improper_command "prf" "print proof terms of theorems" Keyword.diag

   904     (opt_modes -- Scan.option Parse_Spec.xthms1

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

   907 val _ =

   908   Outer_Syntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag

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

   911 val _ =

   912   Outer_Syntax.improper_command "prop" "read and print proposition" Keyword.diag

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

   915 val _ =

   916   Outer_Syntax.improper_command "term" "read and print term" Keyword.diag

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

   919 val _ =

   920   Outer_Syntax.improper_command "typ" "read and print type" Keyword.diag

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

   923 val _ =

   924   Outer_Syntax.improper_command "print_codesetup" "print code generator setup" Keyword.diag

   925     (Scan.succeed

   926       (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep

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

   929 val _ =

   930   Outer_Syntax.improper_command "unused_thms" "find unused theorems" Keyword.diag

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

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

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

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

   939 val _ =

   940   Outer_Syntax.improper_command "cd" "change current working directory" Keyword.control

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

   943 val _ =

   944   Outer_Syntax.improper_command "pwd" "print current working directory" Keyword.diag

   945     (Scan.succeed (Toplevel.no_timing o

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

   948 val _ =

   949   Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.control

   950     (Parse.name >> (fn name =>

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

   953 val _ =

   954   Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.control

   955     (Parse.name >> (fn name =>

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

   958 val _ =

   959   Outer_Syntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"

   960     Keyword.control (Parse.name >> (fn name =>

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

   963 val _ =

   964   Outer_Syntax.improper_command "display_drafts" "display raw source files with symbols"

   965     Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));

   967 val _ =

   968   Outer_Syntax.improper_command "print_drafts" "print raw source files with symbols"

   969     Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));

   971 val _ =  (* FIXME tty only *)

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

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

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

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

   976         Toplevel.quiet := false;

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

   979 val _ =

   980   Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.control

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

   983 val _ =

   984   Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.control

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

   987 val _ =

   988   Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.control

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

   991 val _ =

   992   Outer_Syntax.improper_command "quit" "quit Isabelle" Keyword.control

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

   995 val _ =

   996   Outer_Syntax.improper_command "exit" "exit Isar loop" Keyword.control

   997     (Scan.succeed

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

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

  1000           raise Runtime.TERMINATE))));

  1002 end;

author	wenzelm
	Thu, 15 Mar 2012 22:08:53 +0100
changeset 47824	d0181abdbdac
parent 47821	b8c7eb0c2f89
child 47829	0ec8f04e753a
permissions	-rw-r--r--