src/Pure/Isar/isar_syn.ML
author wenzelm
Fri May 17 20:53:28 2013 +0200 (2013-05-17)
changeset 52060 179236c82c2a
parent 51979 4f3a5f4c1169
child 52143 36ffe23b25f8
permissions -rw-r--r--
renamed 'print_configs' to 'print_options';
wenzelm@5832
     1
(*  Title:      Pure/Isar/isar_syn.ML
wenzelm@5832
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@5832
     3
wenzelm@6353
     4
Isar/Pure outer syntax.
wenzelm@5832
     5
*)
wenzelm@5832
     6
wenzelm@37216
     7
structure Isar_Syn: sig end =
wenzelm@5832
     8
struct
wenzelm@5832
     9
wenzelm@7749
    10
(** markup commands **)
wenzelm@5832
    11
wenzelm@46961
    12
val _ =
wenzelm@46961
    13
  Outer_Syntax.markup_command Thy_Output.Markup
wenzelm@48642
    14
    @{command_spec "header"} "theory header"
wenzelm@51627
    15
    (Parse.document_source >> Isar_Cmd.header_markup);
wenzelm@6353
    16
wenzelm@46961
    17
val _ =
wenzelm@46961
    18
  Outer_Syntax.markup_command Thy_Output.Markup
wenzelm@48642
    19
    @{command_spec "chapter"} "chapter heading"
wenzelm@51627
    20
    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
wenzelm@5958
    21
wenzelm@46961
    22
val _ =
wenzelm@46961
    23
  Outer_Syntax.markup_command Thy_Output.Markup
wenzelm@48642
    24
    @{command_spec "section"} "section heading"
wenzelm@51627
    25
    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
wenzelm@5958
    26
wenzelm@46961
    27
val _ =
wenzelm@46961
    28
  Outer_Syntax.markup_command Thy_Output.Markup
wenzelm@48642
    29
    @{command_spec "subsection"} "subsection heading"
wenzelm@51627
    30
    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
wenzelm@46961
    31
wenzelm@46961
    32
val _ =
wenzelm@46961
    33
  Outer_Syntax.markup_command Thy_Output.Markup
wenzelm@48642
    34
    @{command_spec "subsubsection"} "subsubsection heading"
wenzelm@51627
    35
    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
wenzelm@5958
    36
wenzelm@24868
    37
val _ =
wenzelm@46961
    38
  Outer_Syntax.markup_command Thy_Output.MarkupEnv
wenzelm@48642
    39
    @{command_spec "text"} "formal comment (theory)"
wenzelm@51627
    40
    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
wenzelm@7172
    41
wenzelm@46961
    42
val _ =
wenzelm@46961
    43
  Outer_Syntax.markup_command Thy_Output.Verbatim
wenzelm@48642
    44
    @{command_spec "text_raw"} "raw document preparation text"
wenzelm@51627
    45
    (Parse.opt_target -- Parse.document_source >> Isar_Cmd.local_theory_markup);
wenzelm@7172
    46
wenzelm@46961
    47
val _ =
wenzelm@46961
    48
  Outer_Syntax.markup_command Thy_Output.Markup
wenzelm@48642
    49
    @{command_spec "sect"} "formal comment (proof)"
wenzelm@51627
    50
    (Parse.document_source >> Isar_Cmd.proof_markup);
wenzelm@7172
    51
wenzelm@46961
    52
val _ =
wenzelm@46961
    53
  Outer_Syntax.markup_command Thy_Output.Markup
wenzelm@48642
    54
    @{command_spec "subsect"} "formal comment (proof)"
wenzelm@51627
    55
    (Parse.document_source >> Isar_Cmd.proof_markup);
wenzelm@7172
    56
wenzelm@46961
    57
val _ =
wenzelm@46961
    58
  Outer_Syntax.markup_command Thy_Output.Markup
wenzelm@48642
    59
    @{command_spec "subsubsect"} "formal comment (proof)"
wenzelm@51627
    60
    (Parse.document_source >> Isar_Cmd.proof_markup);
wenzelm@7172
    61
wenzelm@46961
    62
val _ =
wenzelm@46961
    63
  Outer_Syntax.markup_command Thy_Output.MarkupEnv
wenzelm@48642
    64
    @{command_spec "txt"} "formal comment (proof)"
wenzelm@51627
    65
    (Parse.document_source >> Isar_Cmd.proof_markup);
wenzelm@7172
    66
wenzelm@46961
    67
val _ =
wenzelm@46961
    68
  Outer_Syntax.markup_command Thy_Output.Verbatim
wenzelm@48642
    69
    @{command_spec "txt_raw"} "raw document preparation text (proof)"
wenzelm@51627
    70
    (Parse.document_source >> Isar_Cmd.proof_markup);
wenzelm@7775
    71
wenzelm@5832
    72
wenzelm@6886
    73
wenzelm@30142
    74
(** theory commands **)
wenzelm@6886
    75
wenzelm@5832
    76
(* classes and sorts *)
wenzelm@5832
    77
wenzelm@24868
    78
val _ =
wenzelm@48642
    79
  Outer_Syntax.command @{command_spec "classes"} "declare type classes"
wenzelm@48643
    80
    (Scan.repeat1 (Parse.binding -- Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<"}) |--
wenzelm@46922
    81
        Parse.!!! (Parse.list1 Parse.class)) [])
wenzelm@51685
    82
      >> (Toplevel.theory o fold Axclass.axiomatize_class_cmd));
wenzelm@5832
    83
wenzelm@24868
    84
val _ =
wenzelm@48642
    85
  Outer_Syntax.command @{command_spec "classrel"} "state inclusion of type classes (axiomatic!)"
wenzelm@48643
    86
    (Parse.and_list1 (Parse.class -- ((@{keyword "\<subseteq>"} || @{keyword "<"})
wenzelm@46922
    87
        |-- Parse.!!! Parse.class))
wenzelm@51685
    88
    >> (Toplevel.theory o Axclass.axiomatize_classrel_cmd));
wenzelm@5832
    89
wenzelm@24868
    90
val _ =
wenzelm@48642
    91
  Outer_Syntax.local_theory @{command_spec "default_sort"}
wenzelm@46961
    92
    "declare default sort for explicit type variables"
wenzelm@36950
    93
    (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
wenzelm@5832
    94
wenzelm@5832
    95
wenzelm@5832
    96
(* types *)
wenzelm@5832
    97
wenzelm@24868
    98
val _ =
wenzelm@48642
    99
  Outer_Syntax.local_theory @{command_spec "typedecl"} "type declaration"
wenzelm@36950
   100
    (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
wenzelm@35835
   101
      >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
wenzelm@5832
   102
wenzelm@24868
   103
val _ =
wenzelm@48642
   104
  Outer_Syntax.local_theory @{command_spec "type_synonym"} "declare type abbreviation"
wenzelm@45837
   105
    (Parse.type_args -- Parse.binding --
wenzelm@48643
   106
      (@{keyword "="} |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
wenzelm@45837
   107
      >> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
wenzelm@5832
   108
wenzelm@24868
   109
val _ =
wenzelm@48642
   110
  Outer_Syntax.command @{command_spec "nonterminal"}
wenzelm@46961
   111
    "declare syntactic type constructors (grammar nonterminal symbols)"
wenzelm@42375
   112
    (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
wenzelm@5832
   113
wenzelm@24868
   114
val _ =
wenzelm@48642
   115
  Outer_Syntax.command @{command_spec "arities"} "state type arities (axiomatic!)"
wenzelm@51685
   116
    (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold Axclass.axiomatize_arity_cmd));
wenzelm@5832
   117
wenzelm@5832
   118
wenzelm@5832
   119
(* consts and syntax *)
wenzelm@5832
   120
wenzelm@24868
   121
val _ =
wenzelm@48642
   122
  Outer_Syntax.command @{command_spec "judgment"} "declare object-logic judgment"
wenzelm@36950
   123
    (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
wenzelm@8227
   124
wenzelm@24868
   125
val _ =
wenzelm@48642
   126
  Outer_Syntax.command @{command_spec "consts"} "declare constants"
wenzelm@36950
   127
    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));
wenzelm@5832
   128
wenzelm@12142
   129
val mode_spec =
wenzelm@48643
   130
  (@{keyword "output"} >> K ("", false)) ||
wenzelm@48643
   131
    Parse.name -- Scan.optional (@{keyword "output"} >> K false) true;
wenzelm@9731
   132
wenzelm@14900
   133
val opt_mode =
wenzelm@48643
   134
  Scan.optional (@{keyword "("} |-- Parse.!!! (mode_spec --| @{keyword ")"})) Syntax.mode_default;
wenzelm@5832
   135
wenzelm@24868
   136
val _ =
wenzelm@50214
   137
  Outer_Syntax.command @{command_spec "syntax"} "add raw syntax clauses"
wenzelm@42299
   138
    (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax));
wenzelm@5832
   139
wenzelm@24868
   140
val _ =
wenzelm@50214
   141
  Outer_Syntax.command @{command_spec "no_syntax"} "delete raw syntax clauses"
wenzelm@42299
   142
    (opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax));
wenzelm@15748
   143
wenzelm@5832
   144
wenzelm@5832
   145
(* translations *)
wenzelm@5832
   146
wenzelm@5832
   147
val trans_pat =
wenzelm@42326
   148
  Scan.optional
wenzelm@48643
   149
    (@{keyword "("} |-- Parse.!!! (Parse.xname --| @{keyword ")"})) "logic"
wenzelm@42326
   150
    -- Parse.inner_syntax Parse.string;
wenzelm@5832
   151
wenzelm@5832
   152
fun trans_arrow toks =
wenzelm@48643
   153
  ((@{keyword "\<rightharpoonup>"} || @{keyword "=>"}) >> K Syntax.Parse_Rule ||
wenzelm@48643
   154
    (@{keyword "\<leftharpoondown>"} || @{keyword "<="}) >> K Syntax.Print_Rule ||
wenzelm@48643
   155
    (@{keyword "\<rightleftharpoons>"} || @{keyword "=="}) >> K Syntax.Parse_Print_Rule) toks;
wenzelm@5832
   156
wenzelm@5832
   157
val trans_line =
wenzelm@36950
   158
  trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
wenzelm@5832
   159
    >> (fn (left, (arr, right)) => arr (left, right));
wenzelm@5832
   160
wenzelm@24868
   161
val _ =
wenzelm@50214
   162
  Outer_Syntax.command @{command_spec "translations"} "add syntax translation rules"
wenzelm@42204
   163
    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
wenzelm@5832
   164
wenzelm@24868
   165
val _ =
wenzelm@50214
   166
  Outer_Syntax.command @{command_spec "no_translations"} "delete syntax translation rules"
wenzelm@42204
   167
    (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
wenzelm@19260
   168
wenzelm@5832
   169
wenzelm@5832
   170
(* axioms and definitions *)
wenzelm@5832
   171
wenzelm@19631
   172
val opt_unchecked_overloaded =
wenzelm@48643
   173
  Scan.optional (@{keyword "("} |-- Parse.!!!
wenzelm@48643
   174
    (((@{keyword "unchecked"} >> K true) --
wenzelm@48643
   175
        Scan.optional (@{keyword "overloaded"} >> K true) false ||
wenzelm@48643
   176
      @{keyword "overloaded"} >> K (false, true)) --| @{keyword ")"})) (false, false);
wenzelm@19631
   177
wenzelm@24868
   178
val _ =
wenzelm@48642
   179
  Outer_Syntax.command @{command_spec "defs"} "define constants"
wenzelm@35852
   180
    (opt_unchecked_overloaded --
wenzelm@36952
   181
      Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
wenzelm@37216
   182
      >> (Toplevel.theory o Isar_Cmd.add_defs));
wenzelm@6370
   183
wenzelm@14642
   184
wenzelm@21601
   185
(* constant definitions and abbreviations *)
wenzelm@21601
   186
wenzelm@24868
   187
val _ =
wenzelm@48642
   188
  Outer_Syntax.local_theory' @{command_spec "definition"} "constant definition"
wenzelm@44192
   189
    (Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
wenzelm@18780
   190
wenzelm@24868
   191
val _ =
wenzelm@48642
   192
  Outer_Syntax.local_theory' @{command_spec "abbreviation"} "constant abbreviation"
wenzelm@36952
   193
    (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
wenzelm@36950
   194
      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
wenzelm@19659
   195
wenzelm@24868
   196
val _ =
wenzelm@48642
   197
  Outer_Syntax.local_theory @{command_spec "type_notation"}
wenzelm@46961
   198
    "add concrete syntax for type constructors"
wenzelm@42300
   199
    (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
wenzelm@36950
   200
      >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
wenzelm@35413
   201
wenzelm@35413
   202
val _ =
wenzelm@48642
   203
  Outer_Syntax.local_theory @{command_spec "no_type_notation"}
wenzelm@46961
   204
    "delete concrete syntax for type constructors"
wenzelm@42300
   205
    (opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
wenzelm@36950
   206
      >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
wenzelm@35413
   207
wenzelm@35413
   208
val _ =
wenzelm@48642
   209
  Outer_Syntax.local_theory @{command_spec "notation"}
wenzelm@46961
   210
    "add concrete syntax for constants / fixed variables"
wenzelm@51654
   211
    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
wenzelm@36950
   212
      >> (fn (mode, args) => Specification.notation_cmd true mode args));
wenzelm@24950
   213
wenzelm@24950
   214
val _ =
wenzelm@48642
   215
  Outer_Syntax.local_theory @{command_spec "no_notation"}
wenzelm@46961
   216
    "delete concrete syntax for constants / fixed variables"
wenzelm@51654
   217
    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
wenzelm@36950
   218
      >> (fn (mode, args) => Specification.notation_cmd false mode args));
wenzelm@19076
   219
wenzelm@5832
   220
wenzelm@18616
   221
(* constant specifications *)
wenzelm@18616
   222
wenzelm@24868
   223
val _ =
wenzelm@48642
   224
  Outer_Syntax.command @{command_spec "axiomatization"} "axiomatic constant specification"
wenzelm@36950
   225
    (Scan.optional Parse.fixes [] --
wenzelm@36952
   226
      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
wenzelm@36950
   227
      >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
wenzelm@18616
   228
wenzelm@18616
   229
wenzelm@5914
   230
(* theorems *)
wenzelm@5914
   231
wenzelm@26988
   232
fun theorems kind =
wenzelm@45600
   233
  Parse_Spec.name_facts -- Parse.for_fixes
wenzelm@45600
   234
    >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd kind facts fixes);
wenzelm@12712
   235
wenzelm@24868
   236
val _ =
wenzelm@48642
   237
  Outer_Syntax.local_theory' @{command_spec "theorems"} "define theorems"
wenzelm@46961
   238
    (theorems Thm.theoremK);
wenzelm@5914
   239
wenzelm@24868
   240
val _ =
wenzelm@48642
   241
  Outer_Syntax.local_theory' @{command_spec "lemmas"} "define lemmas" (theorems Thm.lemmaK);
wenzelm@5914
   242
wenzelm@24868
   243
val _ =
wenzelm@48642
   244
  Outer_Syntax.local_theory' @{command_spec "declare"} "declare theorems"
wenzelm@45600
   245
    (Parse.and_list1 Parse_Spec.xthms1 -- Parse.for_fixes
wenzelm@45600
   246
      >> (fn (facts, fixes) =>
wenzelm@45600
   247
          #2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
wenzelm@9589
   248
wenzelm@5914
   249
wenzelm@5832
   250
(* name space entry path *)
wenzelm@5832
   251
wenzelm@48645
   252
fun hide_names spec hide what =
wenzelm@48645
   253
  Outer_Syntax.command spec ("hide " ^ what ^ " from name space")
wenzelm@36950
   254
    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
wenzelm@36176
   255
      (Toplevel.theory o uncurry hide));
wenzelm@36176
   256
wenzelm@48645
   257
val _ = hide_names @{command_spec "hide_class"} Isar_Cmd.hide_class "classes";
wenzelm@48645
   258
val _ = hide_names @{command_spec "hide_type"} Isar_Cmd.hide_type "types";
wenzelm@48645
   259
val _ = hide_names @{command_spec "hide_const"} Isar_Cmd.hide_const "constants";
wenzelm@48645
   260
val _ = hide_names @{command_spec "hide_fact"} Isar_Cmd.hide_fact "facts";
wenzelm@5832
   261
wenzelm@5832
   262
wenzelm@5832
   263
(* use ML text *)
wenzelm@5832
   264
wenzelm@24868
   265
val _ =
wenzelm@48642
   266
  Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
wenzelm@36950
   267
    (Parse.ML_source >> (fn (txt, pos) =>
wenzelm@30579
   268
      Toplevel.generic_theory
wenzelm@37949
   269
        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
wenzelm@37949
   270
          Local_Theory.propagate_ml_env)));
wenzelm@30579
   271
wenzelm@30579
   272
val _ =
wenzelm@48642
   273
  Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
wenzelm@36950
   274
    (Parse.ML_source >> (fn (txt, pos) =>
wenzelm@28269
   275
      Toplevel.proof (Proof.map_context (Context.proof_map
wenzelm@37949
   276
        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));
wenzelm@28269
   277
wenzelm@28269
   278
val _ =
wenzelm@48642
   279
  Outer_Syntax.command @{command_spec "ML_val"} "diagnostic ML text"
wenzelm@37216
   280
    (Parse.ML_source >> Isar_Cmd.ml_diag true);
wenzelm@26396
   281
wenzelm@26396
   282
val _ =
wenzelm@48642
   283
  Outer_Syntax.command @{command_spec "ML_command"} "diagnostic ML text (silent)"
wenzelm@51658
   284
    (Parse.ML_source >> Isar_Cmd.ml_diag false);
wenzelm@5832
   285
wenzelm@24868
   286
val _ =
wenzelm@48642
   287
  Outer_Syntax.command @{command_spec "setup"} "ML theory setup"
wenzelm@37216
   288
    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup));
wenzelm@30461
   289
wenzelm@30461
   290
val _ =
wenzelm@48642
   291
  Outer_Syntax.local_theory @{command_spec "local_setup"} "ML local theory setup"
wenzelm@37216
   292
    (Parse.ML_source >> Isar_Cmd.local_setup);
wenzelm@5832
   293
wenzelm@24868
   294
val _ =
wenzelm@48642
   295
  Outer_Syntax.command @{command_spec "attribute_setup"} "define attribute in ML"
wenzelm@42813
   296
    (Parse.position Parse.name --
wenzelm@48643
   297
        Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
wenzelm@36950
   298
      >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
wenzelm@30526
   299
wenzelm@30526
   300
val _ =
wenzelm@48642
   301
  Outer_Syntax.command @{command_spec "method_setup"} "define proof method in ML"
wenzelm@42813
   302
    (Parse.position Parse.name --
wenzelm@48643
   303
        Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
wenzelm@36950
   304
      >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
wenzelm@9197
   305
wenzelm@24868
   306
val _ =
wenzelm@48642
   307
  Outer_Syntax.local_theory @{command_spec "declaration"} "generic ML declaration"
wenzelm@40784
   308
    (Parse.opt_keyword "pervasive" -- Parse.ML_source
wenzelm@40784
   309
      >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
wenzelm@40784
   310
wenzelm@40784
   311
val _ =
wenzelm@48642
   312
  Outer_Syntax.local_theory @{command_spec "syntax_declaration"} "generic ML syntax declaration"
wenzelm@40784
   313
    (Parse.opt_keyword "pervasive" -- Parse.ML_source
wenzelm@40784
   314
      >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
wenzelm@22088
   315
wenzelm@24868
   316
val _ =
wenzelm@48642
   317
  Outer_Syntax.local_theory @{command_spec "simproc_setup"} "define simproc in ML"
wenzelm@42464
   318
    (Parse.position Parse.name --
wenzelm@48643
   319
      (@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword "="}) --
wenzelm@48643
   320
      Parse.ML_source -- Scan.optional (@{keyword "identifier"} |-- Scan.repeat1 Parse.xname) []
wenzelm@37216
   321
    >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
wenzelm@22202
   322
wenzelm@5832
   323
wenzelm@5832
   324
(* translation functions *)
wenzelm@5832
   325
wenzelm@36950
   326
val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
wenzelm@14642
   327
wenzelm@24868
   328
val _ =
wenzelm@48642
   329
  Outer_Syntax.command @{command_spec "parse_ast_translation"}
wenzelm@46961
   330
    "install parse ast translation functions"
wenzelm@37216
   331
    (trfun >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
wenzelm@5832
   332
wenzelm@24868
   333
val _ =
wenzelm@48642
   334
  Outer_Syntax.command @{command_spec "parse_translation"}
wenzelm@46961
   335
    "install parse translation functions"
wenzelm@37216
   336
    (trfun >> (Toplevel.theory o Isar_Cmd.parse_translation));
wenzelm@5832
   337
wenzelm@24868
   338
val _ =
wenzelm@48642
   339
  Outer_Syntax.command @{command_spec "print_translation"}
wenzelm@46961
   340
    "install print translation functions"
wenzelm@37216
   341
    (trfun >> (Toplevel.theory o Isar_Cmd.print_translation));
wenzelm@5832
   342
wenzelm@24868
   343
val _ =
wenzelm@48642
   344
  Outer_Syntax.command @{command_spec "typed_print_translation"}
wenzelm@46961
   345
    "install typed print translation functions"
wenzelm@37216
   346
    (trfun >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
wenzelm@5832
   347
wenzelm@24868
   348
val _ =
wenzelm@48642
   349
  Outer_Syntax.command @{command_spec "print_ast_translation"}
wenzelm@46961
   350
    "install print ast translation functions"
wenzelm@37216
   351
    (trfun >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
wenzelm@5832
   352
wenzelm@5832
   353
wenzelm@5832
   354
(* oracles *)
wenzelm@5832
   355
wenzelm@24868
   356
val _ =
wenzelm@48642
   357
  Outer_Syntax.command @{command_spec "oracle"} "declare oracle"
wenzelm@48643
   358
    (Parse.position Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
wenzelm@37216
   359
      (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
wenzelm@5832
   360
wenzelm@5832
   361
wenzelm@47057
   362
(* bundled declarations *)
wenzelm@47057
   363
wenzelm@47057
   364
val _ =
wenzelm@48642
   365
  Outer_Syntax.local_theory @{command_spec "bundle"} "define bundle of declarations"
wenzelm@48643
   366
    ((Parse.binding --| @{keyword "="}) -- Parse_Spec.xthms1 -- Parse.for_fixes
wenzelm@47057
   367
      >> (uncurry Bundle.bundle_cmd));
wenzelm@47057
   368
wenzelm@47057
   369
val _ =
wenzelm@48642
   370
  Outer_Syntax.command @{command_spec "include"}
wenzelm@47057
   371
    "include declarations from bundle in proof body"
wenzelm@47066
   372
    (Scan.repeat1 (Parse.position Parse.xname)
wenzelm@47066
   373
      >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
wenzelm@47057
   374
wenzelm@47057
   375
val _ =
wenzelm@48642
   376
  Outer_Syntax.command @{command_spec "including"}
wenzelm@47057
   377
    "include declarations from bundle in goal refinement"
wenzelm@47066
   378
    (Scan.repeat1 (Parse.position Parse.xname)
wenzelm@47066
   379
      >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
wenzelm@47066
   380
wenzelm@47066
   381
val _ =
wenzelm@48642
   382
  Outer_Syntax.improper_command @{command_spec "print_bundles"}
wenzelm@48642
   383
    "print bundles of declarations"
wenzelm@51658
   384
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@47057
   385
      Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
wenzelm@47057
   386
wenzelm@47057
   387
wenzelm@47069
   388
(* local theories *)
wenzelm@47069
   389
wenzelm@47069
   390
val _ =
wenzelm@48642
   391
  Outer_Syntax.command @{command_spec "context"} "begin local theory context"
wenzelm@47253
   392
    ((Parse.position Parse.xname >> (fn name =>
wenzelm@47253
   393
        Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
wenzelm@47253
   394
      Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
wenzelm@47253
   395
        >> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
wenzelm@47069
   396
      --| Parse.begin);
wenzelm@47069
   397
wenzelm@47069
   398
wenzelm@12061
   399
(* locales *)
wenzelm@12061
   400
wenzelm@12758
   401
val locale_val =
wenzelm@36952
   402
  Parse_Spec.locale_expression false --
wenzelm@48643
   403
    Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
wenzelm@36952
   404
  Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
wenzelm@12061
   405
wenzelm@24868
   406
val _ =
wenzelm@48642
   407
  Outer_Syntax.command @{command_spec "locale"} "define named proof context"
wenzelm@36950
   408
    (Parse.binding --
wenzelm@48643
   409
      Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
haftmann@27681
   410
      >> (fn ((name, (expr, elems)), begin) =>
wenzelm@21843
   411
          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
wenzelm@41585
   412
            (Expression.add_locale_cmd I name Binding.empty expr elems #> snd)));
ballarin@28085
   413
ballarin@41270
   414
fun parse_interpretation_arguments mandatory =
ballarin@41270
   415
  Parse.!!! (Parse_Spec.locale_expression mandatory) --
ballarin@41270
   416
    Scan.optional
ballarin@41270
   417
      (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
ballarin@41270
   418
wenzelm@24868
   419
val _ =
wenzelm@48642
   420
  Outer_Syntax.command @{command_spec "sublocale"}
wenzelm@46961
   421
    "prove sublocale relation between a locale and a locale expression"
haftmann@51737
   422
    ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
ballarin@41270
   423
      parse_interpretation_arguments false
ballarin@41270
   424
      >> (fn (loc, (expr, equations)) =>
haftmann@51737
   425
          Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_global_cmd I loc expr equations)))
haftmann@51737
   426
    || parse_interpretation_arguments false
haftmann@51737
   427
      >> (fn (expr, equations) => Toplevel.print o
haftmann@51737
   428
          Toplevel.local_theory_to_proof NONE (Expression.sublocale_cmd expr equations)));
ballarin@28895
   429
ballarin@28895
   430
val _ =
wenzelm@48642
   431
  Outer_Syntax.command @{command_spec "interpretation"}
haftmann@51737
   432
    "prove interpretation of locale expression in local theory"
ballarin@41270
   433
    (parse_interpretation_arguments true
wenzelm@30727
   434
      >> (fn (expr, equations) => Toplevel.print o
haftmann@51737
   435
          Toplevel.local_theory_to_proof NONE (Expression.interpretation_cmd expr equations)));
ballarin@29223
   436
ballarin@29223
   437
val _ =
wenzelm@48642
   438
  Outer_Syntax.command @{command_spec "interpret"}
ballarin@29223
   439
    "prove interpretation of locale expression in proof context"
ballarin@41270
   440
    (parse_interpretation_arguments true
ballarin@38108
   441
      >> (fn (expr, equations) => Toplevel.print o
ballarin@38108
   442
          Toplevel.proof' (Expression.interpret_cmd expr equations)));
ballarin@29223
   443
wenzelm@15703
   444
haftmann@22299
   445
(* classes *)
haftmann@22299
   446
wenzelm@24868
   447
val class_val =
wenzelm@46922
   448
  Parse_Spec.class_expression --
wenzelm@48643
   449
    Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
wenzelm@36952
   450
  Scan.repeat1 Parse_Spec.context_element >> pair [];
haftmann@22299
   451
wenzelm@24868
   452
val _ =
wenzelm@48642
   453
  Outer_Syntax.command @{command_spec "class"} "define type class"
wenzelm@48643
   454
   (Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
haftmann@26516
   455
    >> (fn ((name, (supclasses, elems)), begin) =>
wenzelm@24938
   456
        (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
wenzelm@41585
   457
          (Class_Declaration.class_cmd I name supclasses elems #> snd)));
haftmann@22299
   458
wenzelm@24868
   459
val _ =
wenzelm@48642
   460
  Outer_Syntax.local_theory_to_proof @{command_spec "subclass"} "prove a subclass relation"
wenzelm@46922
   461
    (Parse.class >> Class_Declaration.subclass_cmd I);
haftmann@24914
   462
haftmann@24914
   463
val _ =
wenzelm@48642
   464
  Outer_Syntax.command @{command_spec "instantiation"} "instantiate and prove type arity"
wenzelm@36950
   465
   (Parse.multi_arity --| Parse.begin
haftmann@25462
   466
     >> (fn arities => Toplevel.print o
haftmann@38348
   467
         Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
haftmann@24589
   468
haftmann@25485
   469
val _ =
wenzelm@48642
   470
  Outer_Syntax.command @{command_spec "instance"} "prove type arity or subclass relation"
wenzelm@46922
   471
  ((Parse.class --
wenzelm@48643
   472
    ((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
wenzelm@36950
   473
    Parse.multi_arity >> Class.instance_arity_cmd)
wenzelm@36950
   474
    >> (Toplevel.print oo Toplevel.theory_to_proof) ||
wenzelm@36950
   475
    Scan.succeed
wenzelm@36950
   476
      (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
haftmann@22299
   477
haftmann@22299
   478
haftmann@25519
   479
(* arbitrary overloading *)
haftmann@25519
   480
haftmann@25519
   481
val _ =
wenzelm@48642
   482
  Outer_Syntax.command @{command_spec "overloading"} "overloaded definitions"
wenzelm@48643
   483
   (Scan.repeat1 (Parse.name --| (@{keyword "\<equiv>"} || @{keyword "=="}) -- Parse.term --
wenzelm@48643
   484
      Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true
wenzelm@36950
   485
      >> Parse.triple1) --| Parse.begin
haftmann@25519
   486
   >> (fn operations => Toplevel.print o
haftmann@38342
   487
         Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
haftmann@25519
   488
haftmann@25519
   489
wenzelm@22866
   490
(* code generation *)
wenzelm@22866
   491
wenzelm@24868
   492
val _ =
wenzelm@48642
   493
  Outer_Syntax.command @{command_spec "code_datatype"}
wenzelm@46961
   494
    "define set of code datatype constructors"
wenzelm@36950
   495
    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
wenzelm@22866
   496
wenzelm@22866
   497
wenzelm@5832
   498
wenzelm@5832
   499
(** proof commands **)
wenzelm@5832
   500
wenzelm@5832
   501
(* statements *)
wenzelm@5832
   502
wenzelm@48645
   503
fun gen_theorem spec schematic kind =
wenzelm@48645
   504
  Outer_Syntax.local_theory_to_proof' spec
wenzelm@36317
   505
    ("state " ^ (if schematic then "schematic " ^ kind else kind))
wenzelm@36952
   506
    (Scan.optional (Parse_Spec.opt_thm_name ":" --|
wenzelm@47067
   507
      Scan.ahead (Parse_Spec.includes >> K "" ||
wenzelm@47067
   508
        Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
wenzelm@47067
   509
      Scan.optional Parse_Spec.includes [] --
wenzelm@47067
   510
      Parse_Spec.general_statement >> (fn ((a, includes), (elems, concl)) =>
wenzelm@36317
   511
        ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
wenzelm@47067
   512
          kind NONE (K I) a includes elems concl)));
wenzelm@5832
   513
wenzelm@48645
   514
val _ = gen_theorem @{command_spec "theorem"} false Thm.theoremK;
wenzelm@48645
   515
val _ = gen_theorem @{command_spec "lemma"} false Thm.lemmaK;
wenzelm@48645
   516
val _ = gen_theorem @{command_spec "corollary"} false Thm.corollaryK;
wenzelm@48645
   517
val _ = gen_theorem @{command_spec "schematic_theorem"} true Thm.theoremK;
wenzelm@48645
   518
val _ = gen_theorem @{command_spec "schematic_lemma"} true Thm.lemmaK;
wenzelm@48645
   519
val _ = gen_theorem @{command_spec "schematic_corollary"} true Thm.corollaryK;
wenzelm@5832
   520
wenzelm@24868
   521
val _ =
wenzelm@48642
   522
  Outer_Syntax.local_theory_to_proof @{command_spec "notepad"} "begin proof context"
wenzelm@40960
   523
    (Parse.begin >> K Proof.begin_notepad);
wenzelm@40960
   524
wenzelm@40960
   525
val _ =
wenzelm@48642
   526
  Outer_Syntax.command @{command_spec "have"} "state local goal"
wenzelm@37216
   527
    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
wenzelm@17353
   528
wenzelm@24868
   529
val _ =
wenzelm@50214
   530
  Outer_Syntax.command @{command_spec "hence"} "old-style alias of \"then have\""
wenzelm@37216
   531
    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
wenzelm@17353
   532
wenzelm@24868
   533
val _ =
wenzelm@48642
   534
  Outer_Syntax.command @{command_spec "show"}
wenzelm@46961
   535
    "state local goal, solving current obligation"
wenzelm@37216
   536
    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
wenzelm@5832
   537
wenzelm@24868
   538
val _ =
wenzelm@50214
   539
  Outer_Syntax.command @{command_spec "thus"} "old-style alias of  \"then show\""
wenzelm@37216
   540
    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
wenzelm@6501
   541
wenzelm@5832
   542
wenzelm@5914
   543
(* facts *)
wenzelm@5832
   544
wenzelm@36952
   545
val facts = Parse.and_list1 Parse_Spec.xthms1;
wenzelm@9197
   546
wenzelm@24868
   547
val _ =
wenzelm@48642
   548
  Outer_Syntax.command @{command_spec "then"} "forward chaining"
wenzelm@17900
   549
    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
wenzelm@5832
   550
wenzelm@24868
   551
val _ =
wenzelm@48642
   552
  Outer_Syntax.command @{command_spec "from"} "forward chaining from given facts"
wenzelm@36323
   553
    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
wenzelm@5914
   554
wenzelm@24868
   555
val _ =
wenzelm@48642
   556
  Outer_Syntax.command @{command_spec "with"} "forward chaining from given and current facts"
wenzelm@36323
   557
    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
wenzelm@6878
   558
wenzelm@24868
   559
val _ =
wenzelm@48642
   560
  Outer_Syntax.command @{command_spec "note"} "define facts"
wenzelm@36952
   561
    (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
wenzelm@5832
   562
wenzelm@24868
   563
val _ =
wenzelm@48642
   564
  Outer_Syntax.command @{command_spec "using"} "augment goal facts"
wenzelm@36323
   565
    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
wenzelm@18544
   566
wenzelm@24868
   567
val _ =
wenzelm@48642
   568
  Outer_Syntax.command @{command_spec "unfolding"} "unfold definitions in goal and facts"
wenzelm@36323
   569
    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
wenzelm@12926
   570
wenzelm@5832
   571
wenzelm@5832
   572
(* proof context *)
wenzelm@5832
   573
wenzelm@24868
   574
val _ =
wenzelm@48642
   575
  Outer_Syntax.command @{command_spec "fix"} "fix local variables (Skolem constants)"
wenzelm@36950
   576
    (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
wenzelm@11890
   577
wenzelm@24868
   578
val _ =
wenzelm@48642
   579
  Outer_Syntax.command @{command_spec "assume"} "assume propositions"
wenzelm@36952
   580
    (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
wenzelm@5832
   581
wenzelm@24868
   582
val _ =
wenzelm@48642
   583
  Outer_Syntax.command @{command_spec "presume"} "assume propositions, to be established later"
wenzelm@36952
   584
    (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
wenzelm@6850
   585
wenzelm@24868
   586
val _ =
wenzelm@50214
   587
  Outer_Syntax.command @{command_spec "def"} "local definition (non-polymorphic)"
wenzelm@36950
   588
    (Parse.and_list1
wenzelm@36952
   589
      (Parse_Spec.opt_thm_name ":" --
wenzelm@36950
   590
        ((Parse.binding -- Parse.opt_mixfix) --
wenzelm@48643
   591
          ((@{keyword "\<equiv>"} || @{keyword "=="}) |-- Parse.!!! Parse.termp)))
wenzelm@36323
   592
    >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
wenzelm@6953
   593
wenzelm@24868
   594
val _ =
wenzelm@48642
   595
  Outer_Syntax.command @{command_spec "obtain"} "generalized elimination"
wenzelm@36952
   596
    (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
wenzelm@36323
   597
      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
wenzelm@5832
   598
wenzelm@24868
   599
val _ =
wenzelm@48642
   600
  Outer_Syntax.command @{command_spec "guess"} "wild guessing (unstructured)"
wenzelm@36950
   601
    (Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
wenzelm@17854
   602
wenzelm@24868
   603
val _ =
wenzelm@48642
   604
  Outer_Syntax.command @{command_spec "let"} "bind text variables"
wenzelm@48643
   605
    (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword "="} |-- Parse.term))
wenzelm@36323
   606
      >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
wenzelm@5832
   607
wenzelm@36505
   608
val _ =
wenzelm@48642
   609
  Outer_Syntax.command @{command_spec "write"} "add concrete syntax for constants / fixed variables"
wenzelm@51654
   610
    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
wenzelm@36505
   611
    >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
wenzelm@36505
   612
wenzelm@11793
   613
val case_spec =
wenzelm@48643
   614
  (@{keyword "("} |--
wenzelm@48643
   615
    Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.binding) --| @{keyword ")"}) ||
wenzelm@36952
   616
    Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1;
wenzelm@11793
   617
wenzelm@24868
   618
val _ =
wenzelm@48642
   619
  Outer_Syntax.command @{command_spec "case"} "invoke local context"
wenzelm@36323
   620
    (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
wenzelm@8370
   621
wenzelm@5832
   622
wenzelm@5832
   623
(* proof structure *)
wenzelm@5832
   624
wenzelm@24868
   625
val _ =
wenzelm@48642
   626
  Outer_Syntax.command @{command_spec "{"} "begin explicit proof block"
wenzelm@17900
   627
    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
wenzelm@5832
   628
wenzelm@24868
   629
val _ =
wenzelm@48642
   630
  Outer_Syntax.command @{command_spec "}"} "end explicit proof block"
wenzelm@20305
   631
    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
wenzelm@6687
   632
wenzelm@24868
   633
val _ =
wenzelm@48642
   634
  Outer_Syntax.command @{command_spec "next"} "enter next proof block"
wenzelm@17900
   635
    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
wenzelm@5832
   636
wenzelm@5832
   637
wenzelm@5832
   638
(* end proof *)
wenzelm@5832
   639
wenzelm@24868
   640
val _ =
wenzelm@50214
   641
  Outer_Syntax.command @{command_spec "qed"} "conclude proof"
wenzelm@37216
   642
    (Scan.option Method.parse >> Isar_Cmd.qed);
wenzelm@5832
   643
wenzelm@24868
   644
val _ =
wenzelm@48642
   645
  Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
wenzelm@37216
   646
    (Method.parse -- Scan.option Method.parse >> Isar_Cmd.terminal_proof);
wenzelm@6404
   647
wenzelm@24868
   648
val _ =
wenzelm@48642
   649
  Outer_Syntax.command @{command_spec ".."} "default proof"
wenzelm@37216
   650
    (Scan.succeed Isar_Cmd.default_proof);
wenzelm@8966
   651
wenzelm@24868
   652
val _ =
wenzelm@48642
   653
  Outer_Syntax.command @{command_spec "."} "immediate proof"
wenzelm@37216
   654
    (Scan.succeed Isar_Cmd.immediate_proof);
wenzelm@6404
   655
wenzelm@24868
   656
val _ =
wenzelm@48642
   657
  Outer_Syntax.command @{command_spec "done"} "done proof"
wenzelm@37216
   658
    (Scan.succeed Isar_Cmd.done_proof);
wenzelm@5832
   659
wenzelm@24868
   660
val _ =
wenzelm@48642
   661
  Outer_Syntax.command @{command_spec "sorry"} "skip proof (quick-and-dirty mode only!)"
wenzelm@37216
   662
    (Scan.succeed Isar_Cmd.skip_proof);
wenzelm@6888
   663
wenzelm@24868
   664
val _ =
wenzelm@48642
   665
  Outer_Syntax.command @{command_spec "oops"} "forget proof"
wenzelm@18561
   666
    (Scan.succeed Toplevel.forget_proof);
wenzelm@8210
   667
wenzelm@5832
   668
wenzelm@5832
   669
(* proof steps *)
wenzelm@5832
   670
wenzelm@24868
   671
val _ =
wenzelm@48642
   672
  Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
wenzelm@49865
   673
    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.print o Toplevel.proof (Proof.defer n)));
wenzelm@8165
   674
wenzelm@24868
   675
val _ =
wenzelm@48642
   676
  Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
wenzelm@49865
   677
    (Parse.nat >> (fn n => Toplevel.print o Toplevel.proof (Proof.prefer n)));
wenzelm@8165
   678
wenzelm@24868
   679
val _ =
wenzelm@48642
   680
  Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
wenzelm@49863
   681
    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_results)));
wenzelm@5832
   682
wenzelm@24868
   683
val _ =
wenzelm@50214
   684
  Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
wenzelm@49863
   685
    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end_results)));
wenzelm@5832
   686
wenzelm@24868
   687
val _ =
wenzelm@50214
   688
  Outer_Syntax.command @{command_spec "proof"} "backward proof step"
wenzelm@22117
   689
    (Scan.option Method.parse >> (fn m => Toplevel.print o
wenzelm@49863
   690
      Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
wenzelm@27563
   691
      Toplevel.skip_proof (fn i => i + 1)));
wenzelm@5832
   692
wenzelm@5832
   693
wenzelm@6773
   694
(* calculational proof commands *)
wenzelm@6773
   695
wenzelm@6878
   696
val calc_args =
wenzelm@48643
   697
  Scan.option (@{keyword "("} |-- Parse.!!! ((Parse_Spec.xthms1 --| @{keyword ")"})));
wenzelm@6878
   698
wenzelm@24868
   699
val _ =
wenzelm@48642
   700
  Outer_Syntax.command @{command_spec "also"} "combine calculation and current facts"
wenzelm@49868
   701
    (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
wenzelm@6773
   702
wenzelm@24868
   703
val _ =
wenzelm@48642
   704
  Outer_Syntax.command @{command_spec "finally"}
wenzelm@46961
   705
    "combine calculation and current facts, exhibit result"
wenzelm@49868
   706
    (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
wenzelm@6773
   707
wenzelm@24868
   708
val _ =
wenzelm@48642
   709
  Outer_Syntax.command @{command_spec "moreover"} "augment calculation by current facts"
wenzelm@17900
   710
    (Scan.succeed (Toplevel.proof' Calculation.moreover));
wenzelm@8562
   711
wenzelm@24868
   712
val _ =
wenzelm@48642
   713
  Outer_Syntax.command @{command_spec "ultimately"}
wenzelm@46961
   714
    "augment calculation by current facts, exhibit result"
wenzelm@17900
   715
    (Scan.succeed (Toplevel.proof' Calculation.ultimately));
wenzelm@8588
   716
wenzelm@6773
   717
wenzelm@6742
   718
(* proof navigation *)
wenzelm@5944
   719
wenzelm@24868
   720
val _ =
wenzelm@48642
   721
  Outer_Syntax.command @{command_spec "back"} "backtracking of proof command"
wenzelm@33390
   722
    (Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I));
wenzelm@6742
   723
haftmann@22744
   724
wenzelm@27614
   725
(* nested commands *)
wenzelm@25578
   726
wenzelm@29309
   727
val props_text =
wenzelm@43775
   728
  Scan.optional Parse.properties [] -- Parse.position Parse.string
wenzelm@36950
   729
  >> (fn (props, (str, pos)) =>
wenzelm@36950
   730
      (Position.of_properties (Position.default_properties pos props), str));
wenzelm@29309
   731
wenzelm@25578
   732
val _ =
wenzelm@50214
   733
  Outer_Syntax.improper_command @{command_spec "Isabelle.command"} "evaluate nested Isabelle command"
wenzelm@29309
   734
    (props_text :|-- (fn (pos, str) =>
wenzelm@36953
   735
      (case Outer_Syntax.parse pos str of
wenzelm@27838
   736
        [tr] => Scan.succeed (K tr)
wenzelm@43947
   737
      | _ => Scan.fail_with (K (fn () => "exactly one command expected")))
wenzelm@43947
   738
      handle ERROR msg => Scan.fail_with (K (fn () => msg))));
wenzelm@25578
   739
wenzelm@25578
   740
haftmann@22744
   741
wenzelm@5832
   742
(** diagnostic commands (for interactive mode only) **)
wenzelm@5832
   743
wenzelm@36950
   744
val opt_modes =
wenzelm@48643
   745
  Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
wenzelm@36950
   746
wenzelm@48643
   747
val opt_bang = Scan.optional (@{keyword "!"} >> K true) false;
wenzelm@8464
   748
wenzelm@24868
   749
val _ =
wenzelm@48642
   750
  Outer_Syntax.improper_command @{command_spec "pretty_setmargin"}
wenzelm@46961
   751
    "change default margin for pretty printing"
wenzelm@51658
   752
    (Parse.nat >> (fn n => Toplevel.imperative (fn () => Pretty.margin_default := n)));
wenzelm@7124
   753
wenzelm@24868
   754
val _ =
wenzelm@50213
   755
  Outer_Syntax.improper_command @{command_spec "help"}
wenzelm@50213
   756
    "retrieve outer syntax commands according to name patterns"
wenzelm@51658
   757
    (Scan.repeat Parse.name >>
wenzelm@51658
   758
      (fn pats => Toplevel.imperative (fn () => Outer_Syntax.help_outer_syntax pats)));
wenzelm@21714
   759
wenzelm@24868
   760
val _ =
wenzelm@48642
   761
  Outer_Syntax.improper_command @{command_spec "print_commands"} "print outer syntax commands"
wenzelm@51658
   762
    (Scan.succeed (Toplevel.imperative Outer_Syntax.print_outer_syntax));
wenzelm@5832
   763
wenzelm@24868
   764
val _ =
wenzelm@52060
   765
  Outer_Syntax.improper_command @{command_spec "print_options"} "print configuration options"
wenzelm@51658
   766
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@52060
   767
      Toplevel.keep (Attrib.print_options o Toplevel.context_of)));
wenzelm@23989
   768
wenzelm@24868
   769
val _ =
wenzelm@50737
   770
  Outer_Syntax.improper_command @{command_spec "print_context"} "print main context"
wenzelm@51658
   771
    (Scan.succeed (Toplevel.keep Toplevel.print_state_context));
wenzelm@7308
   772
wenzelm@24868
   773
val _ =
wenzelm@48642
   774
  Outer_Syntax.improper_command @{command_spec "print_theory"}
wenzelm@46961
   775
    "print logical theory contents (verbose!)"
wenzelm@51658
   776
    (opt_bang >> (fn b => Toplevel.unknown_theory o
wenzelm@50737
   777
      Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
wenzelm@5832
   778
wenzelm@24868
   779
val _ =
wenzelm@48642
   780
  Outer_Syntax.improper_command @{command_spec "print_syntax"}
wenzelm@46961
   781
    "print inner syntax of context (verbose!)"
wenzelm@51658
   782
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@50737
   783
      Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
wenzelm@5832
   784
wenzelm@24868
   785
val _ =
wenzelm@51585
   786
  Outer_Syntax.improper_command @{command_spec "print_defn_rules"}
wenzelm@51585
   787
    "print definitional rewrite rules of context"
wenzelm@51658
   788
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@51585
   789
      Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
wenzelm@51585
   790
wenzelm@51585
   791
val _ =
wenzelm@48642
   792
  Outer_Syntax.improper_command @{command_spec "print_abbrevs"}
wenzelm@51585
   793
    "print constant abbreviations of context"
wenzelm@51658
   794
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@50737
   795
      Toplevel.keep (Proof_Context.print_abbrevs o Toplevel.context_of)));
wenzelm@21726
   796
wenzelm@24868
   797
val _ =
wenzelm@48642
   798
  Outer_Syntax.improper_command @{command_spec "print_theorems"}
wenzelm@46961
   799
    "print theorems of local theory or proof context"
wenzelm@51658
   800
    (opt_bang >> Isar_Cmd.print_theorems);
wenzelm@5881
   801
wenzelm@24868
   802
val _ =
wenzelm@48642
   803
  Outer_Syntax.improper_command @{command_spec "print_locales"}
wenzelm@46961
   804
    "print locales of this theory"
wenzelm@51658
   805
    (Scan.succeed (Toplevel.unknown_theory o
wenzelm@50737
   806
      Toplevel.keep (Locale.print_locales o Toplevel.theory_of)));
wenzelm@12061
   807
wenzelm@24868
   808
val _ =
wenzelm@48642
   809
  Outer_Syntax.improper_command @{command_spec "print_classes"}
wenzelm@48642
   810
    "print classes of this theory"
wenzelm@51658
   811
    (Scan.succeed (Toplevel.unknown_theory o
wenzelm@42359
   812
      Toplevel.keep (Class.print_classes o Toplevel.context_of)));
haftmann@22744
   813
wenzelm@24868
   814
val _ =
wenzelm@48642
   815
  Outer_Syntax.improper_command @{command_spec "print_locale"}
wenzelm@48642
   816
    "print locale of this theory"
wenzelm@50737
   817
    (opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
wenzelm@51658
   818
      Toplevel.unknown_theory o
wenzelm@50737
   819
      Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
wenzelm@12061
   820
wenzelm@24868
   821
val _ =
wenzelm@48642
   822
  Outer_Syntax.improper_command @{command_spec "print_interps"}
wenzelm@46961
   823
    "print interpretations of locale for this theory or proof context"
wenzelm@51658
   824
    (Parse.position Parse.xname >> (fn name =>
wenzelm@51658
   825
      Toplevel.unknown_context o
wenzelm@50737
   826
      Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
ballarin@32804
   827
ballarin@32804
   828
val _ =
wenzelm@48642
   829
  Outer_Syntax.improper_command @{command_spec "print_dependencies"}
wenzelm@46961
   830
    "print dependencies of locale expression"
wenzelm@51658
   831
    (opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
wenzelm@51658
   832
      Toplevel.unknown_context o
wenzelm@51658
   833
      Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
ballarin@41435
   834
ballarin@41435
   835
val _ =
wenzelm@48642
   836
  Outer_Syntax.improper_command @{command_spec "print_attributes"}
wenzelm@46961
   837
    "print attributes of this theory"
wenzelm@51658
   838
    (Scan.succeed (Toplevel.unknown_theory o
wenzelm@50737
   839
      Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of)));
wenzelm@5832
   840
wenzelm@24868
   841
val _ =
wenzelm@48642
   842
  Outer_Syntax.improper_command @{command_spec "print_simpset"}
wenzelm@46961
   843
    "print context of Simplifier"
wenzelm@51658
   844
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@51717
   845
      Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset o Toplevel.context_of)));
wenzelm@16027
   846
wenzelm@24868
   847
val _ =
wenzelm@48642
   848
  Outer_Syntax.improper_command @{command_spec "print_rules"} "print intro/elim rules"
wenzelm@51658
   849
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@50737
   850
      Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
wenzelm@12383
   851
wenzelm@24868
   852
val _ =
wenzelm@48642
   853
  Outer_Syntax.improper_command @{command_spec "print_trans_rules"} "print transitivity rules"
wenzelm@51658
   854
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@50737
   855
      Toplevel.keep (Calculation.print_rules o Toplevel.context_of)));
wenzelm@9221
   856
wenzelm@24868
   857
val _ =
wenzelm@48642
   858
  Outer_Syntax.improper_command @{command_spec "print_methods"} "print methods of this theory"
wenzelm@51658
   859
    (Scan.succeed (Toplevel.unknown_theory o
wenzelm@50737
   860
      Toplevel.keep (Method.print_methods o Toplevel.theory_of)));
wenzelm@5832
   861
wenzelm@24868
   862
val _ =
wenzelm@50214
   863
  Outer_Syntax.improper_command @{command_spec "print_antiquotations"} "print antiquotations"
wenzelm@51658
   864
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@50737
   865
      Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of)));
wenzelm@9221
   866
wenzelm@24868
   867
val _ =
wenzelm@48642
   868
  Outer_Syntax.improper_command @{command_spec "thy_deps"} "visualize theory dependencies"
wenzelm@51658
   869
    (Scan.succeed Isar_Cmd.thy_deps);
haftmann@22485
   870
wenzelm@24868
   871
val _ =
wenzelm@49569
   872
  Outer_Syntax.improper_command @{command_spec "locale_deps"} "visualize locale dependencies"
wenzelm@51658
   873
    (Scan.succeed Isar_Cmd.locale_deps);
wenzelm@49569
   874
wenzelm@49569
   875
val _ =
wenzelm@48642
   876
  Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
wenzelm@51658
   877
    (Scan.succeed Isar_Cmd.class_deps);
wenzelm@20574
   878
wenzelm@24868
   879
val _ =
wenzelm@48642
   880
  Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
wenzelm@51658
   881
    (Parse_Spec.xthms1 >> Isar_Cmd.thm_deps);
wenzelm@9454
   882
wenzelm@24868
   883
val _ =
wenzelm@48642
   884
  Outer_Syntax.improper_command @{command_spec "print_binds"} "print term bindings of proof context"
wenzelm@51658
   885
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@50737
   886
      Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of)));
wenzelm@5832
   887
wenzelm@24868
   888
val _ =
wenzelm@48642
   889
  Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
wenzelm@51658
   890
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@50737
   891
      Toplevel.keep (Proof_Context.print_lthms o Toplevel.context_of)));
wenzelm@5832
   892
wenzelm@24868
   893
val _ =
wenzelm@48642
   894
  Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
wenzelm@51658
   895
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@50737
   896
      Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of)));
wenzelm@8370
   897
wenzelm@24868
   898
val _ =
wenzelm@48642
   899
  Outer_Syntax.improper_command @{command_spec "print_statement"}
wenzelm@46961
   900
    "print theorems as long statements"
wenzelm@51658
   901
    (opt_modes -- Parse_Spec.xthms1 >> Isar_Cmd.print_stmts);
wenzelm@19269
   902
wenzelm@24868
   903
val _ =
wenzelm@48642
   904
  Outer_Syntax.improper_command @{command_spec "thm"} "print theorems"
wenzelm@51658
   905
    (opt_modes -- Parse_Spec.xthms1 >> Isar_Cmd.print_thms);
wenzelm@5832
   906
wenzelm@24868
   907
val _ =
wenzelm@48642
   908
  Outer_Syntax.improper_command @{command_spec "prf"} "print proof terms of theorems"
wenzelm@51658
   909
    (opt_modes -- Scan.option Parse_Spec.xthms1 >> Isar_Cmd.print_prfs false);
berghofe@11524
   910
wenzelm@24868
   911
val _ =
wenzelm@48642
   912
  Outer_Syntax.improper_command @{command_spec "full_prf"} "print full proof terms of theorems"
wenzelm@51658
   913
    (opt_modes -- Scan.option Parse_Spec.xthms1 >> Isar_Cmd.print_prfs true);
berghofe@11524
   914
wenzelm@24868
   915
val _ =
wenzelm@48642
   916
  Outer_Syntax.improper_command @{command_spec "prop"} "read and print proposition"
wenzelm@51658
   917
    (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
wenzelm@5832
   918
wenzelm@24868
   919
val _ =
wenzelm@48642
   920
  Outer_Syntax.improper_command @{command_spec "term"} "read and print term"
wenzelm@51658
   921
    (opt_modes -- Parse.term >> Isar_Cmd.print_term);
wenzelm@5832
   922
wenzelm@24868
   923
val _ =
wenzelm@48642
   924
  Outer_Syntax.improper_command @{command_spec "typ"} "read and print type"
wenzelm@48792
   925
    (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
wenzelm@51658
   926
      >> Isar_Cmd.print_type);
wenzelm@5832
   927
wenzelm@24868
   928
val _ =
wenzelm@48642
   929
  Outer_Syntax.improper_command @{command_spec "print_codesetup"} "print code generator setup"
wenzelm@51658
   930
    (Scan.succeed (Toplevel.unknown_theory o
wenzelm@51658
   931
      Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
wenzelm@5832
   932
berghofe@26184
   933
val _ =
wenzelm@48642
   934
  Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
wenzelm@36950
   935
    (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
wenzelm@51658
   936
       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> Isar_Cmd.unused_thms);
berghofe@26184
   937
wenzelm@5832
   938
wenzelm@30142
   939
wenzelm@5832
   940
(** system commands (for interactive mode only) **)
wenzelm@5832
   941
wenzelm@24868
   942
val _ =
wenzelm@48642
   943
  Outer_Syntax.improper_command @{command_spec "cd"} "change current working directory"
wenzelm@51658
   944
    (Parse.path >> (fn name => Toplevel.imperative (fn () => File.cd (Path.explode name))));
wenzelm@5832
   945
wenzelm@24868
   946
val _ =
wenzelm@48642
   947
  Outer_Syntax.improper_command @{command_spec "pwd"} "print current working directory"
wenzelm@51658
   948
    (Scan.succeed (Toplevel.imperative (fn () => writeln (Path.print (File.pwd ())))));
wenzelm@5832
   949
wenzelm@24868
   950
val _ =
wenzelm@48642
   951
  Outer_Syntax.improper_command @{command_spec "use_thy"} "use theory file"
wenzelm@51658
   952
    (Parse.position Parse.name >>
wenzelm@51658
   953
      (fn name => Toplevel.imperative (fn () => Thy_Info.use_thy name)));
wenzelm@5832
   954
wenzelm@24868
   955
val _ =
wenzelm@48642
   956
  Outer_Syntax.improper_command @{command_spec "remove_thy"} "remove theory from loader database"
wenzelm@51658
   957
    (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
wenzelm@7102
   958
wenzelm@24868
   959
val _ =
wenzelm@48642
   960
  Outer_Syntax.improper_command @{command_spec "kill_thy"}
wenzelm@46961
   961
    "kill theory -- try to remove from loader database"
wenzelm@51658
   962
    (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
wenzelm@7931
   963
wenzelm@24868
   964
val _ =
wenzelm@48642
   965
  Outer_Syntax.improper_command @{command_spec "display_drafts"}
wenzelm@46961
   966
    "display raw source files with symbols"
wenzelm@51658
   967
    (Scan.repeat1 Parse.path >> Isar_Cmd.display_drafts);
wenzelm@14934
   968
wenzelm@24868
   969
val _ =
wenzelm@48642
   970
  Outer_Syntax.improper_command @{command_spec "print_drafts"}
wenzelm@46961
   971
    "print raw source files with symbols"
wenzelm@51658
   972
    (Scan.repeat1 Parse.path >> Isar_Cmd.print_drafts);
wenzelm@14934
   973
wenzelm@39165
   974
val _ =  (* FIXME tty only *)
wenzelm@48642
   975
  Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
wenzelm@39165
   976
    (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
wenzelm@51658
   977
      Toplevel.keep (fn state =>
wenzelm@51979
   978
       (case limit of NONE => () | SOME n => Options.default_put_int @{option goals_limit} n;
wenzelm@39165
   979
        Toplevel.quiet := false;
wenzelm@39165
   980
        Print_Mode.with_modes modes (Toplevel.print_state true) state))));
wenzelm@7199
   981
wenzelm@24868
   982
val _ =
wenzelm@48642
   983
  Outer_Syntax.improper_command @{command_spec "disable_pr"}
wenzelm@46961
   984
    "disable printing of toplevel state"
wenzelm@51658
   985
    (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := true)));
wenzelm@5832
   986
wenzelm@24868
   987
val _ =
wenzelm@48642
   988
  Outer_Syntax.improper_command @{command_spec "enable_pr"}
wenzelm@46961
   989
    "enable printing of toplevel state"
wenzelm@51658
   990
    (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := false)));
wenzelm@7222
   991
wenzelm@24868
   992
val _ =
wenzelm@48642
   993
  Outer_Syntax.improper_command @{command_spec "commit"}
wenzelm@50214
   994
    "commit current session to ML session image"
wenzelm@51658
   995
    (Parse.opt_unit >> K (Toplevel.imperative Secure.commit));
wenzelm@5832
   996
wenzelm@24868
   997
val _ =
wenzelm@48642
   998
  Outer_Syntax.improper_command @{command_spec "quit"} "quit Isabelle"
wenzelm@51658
   999
    (Parse.opt_unit >> (K (Toplevel.imperative quit)));
wenzelm@5832
  1000
wenzelm@24868
  1001
val _ =
wenzelm@48642
  1002
  Outer_Syntax.improper_command @{command_spec "exit"} "exit Isar loop"
wenzelm@37977
  1003
    (Scan.succeed
wenzelm@51658
  1004
      (Toplevel.keep (fn state =>
wenzelm@37977
  1005
        (Context.set_thread_data (try Toplevel.generic_theory_of state);
wenzelm@38888
  1006
          raise Runtime.TERMINATE))));
wenzelm@5832
  1007
wenzelm@48646
  1008
val _ =
wenzelm@48646
  1009
  Outer_Syntax.improper_command @{command_spec "welcome"} "print welcome message"
wenzelm@51658
  1010
    (Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
wenzelm@48646
  1011
wenzelm@48646
  1012
wenzelm@48646
  1013
wenzelm@48646
  1014
(** raw Isar read-eval-print loop **)
wenzelm@48646
  1015
wenzelm@48646
  1016
val _ =
wenzelm@48646
  1017
  Outer_Syntax.improper_command @{command_spec "init_toplevel"} "init toplevel point-of-interest"
wenzelm@51658
  1018
    (Scan.succeed (Toplevel.imperative Isar.init));
wenzelm@48646
  1019
wenzelm@48646
  1020
val _ =
wenzelm@48646
  1021
  Outer_Syntax.improper_command @{command_spec "linear_undo"} "undo commands"
wenzelm@48646
  1022
    (Scan.optional Parse.nat 1 >>
wenzelm@51658
  1023
      (fn n => Toplevel.imperative (fn () => Isar.linear_undo n)));
wenzelm@48646
  1024
wenzelm@48646
  1025
val _ =
wenzelm@48646
  1026
  Outer_Syntax.improper_command @{command_spec "undo"} "undo commands (skipping closed proofs)"
wenzelm@48646
  1027
    (Scan.optional Parse.nat 1 >>
wenzelm@51658
  1028
      (fn n => Toplevel.imperative (fn () => Isar.undo n)));
wenzelm@48646
  1029
wenzelm@48646
  1030
val _ =
wenzelm@48646
  1031
  Outer_Syntax.improper_command @{command_spec "undos_proof"}
wenzelm@48646
  1032
    "undo commands (skipping closed proofs)"
wenzelm@51658
  1033
    (Scan.optional Parse.nat 1 >> (fn n =>
wenzelm@48646
  1034
      Toplevel.keep (fn state =>
wenzelm@48646
  1035
        if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF)));
wenzelm@48646
  1036
wenzelm@48646
  1037
val _ =
wenzelm@48646
  1038
  Outer_Syntax.improper_command @{command_spec "cannot_undo"}
wenzelm@48646
  1039
    "partial undo -- Proof General legacy"
wenzelm@48646
  1040
    (Parse.name >>
wenzelm@51658
  1041
      (fn "end" => Toplevel.imperative (fn () => Isar.undo 1)
wenzelm@48646
  1042
        | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
wenzelm@48646
  1043
wenzelm@48646
  1044
val _ =
wenzelm@48646
  1045
  Outer_Syntax.improper_command @{command_spec "kill"}
wenzelm@48646
  1046
    "kill partial proof or theory development"
wenzelm@51658
  1047
    (Scan.succeed (Toplevel.imperative Isar.kill));
wenzelm@48646
  1048
wenzelm@48646
  1049
wenzelm@48646
  1050
wenzelm@48646
  1051
(** extraction of programs from proofs **)
wenzelm@48646
  1052
wenzelm@48646
  1053
val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
wenzelm@48646
  1054
wenzelm@48646
  1055
val _ =
wenzelm@48646
  1056
  Outer_Syntax.command @{command_spec "realizers"}
wenzelm@48646
  1057
    "specify realizers for primitive axioms / theorems, together with correctness proof"
wenzelm@48646
  1058
    (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
wenzelm@48646
  1059
     (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
wenzelm@48646
  1060
       (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
wenzelm@48646
  1061
wenzelm@48646
  1062
val _ =
wenzelm@48646
  1063
  Outer_Syntax.command @{command_spec "realizability"}
wenzelm@48646
  1064
    "add equations characterizing realizability"
wenzelm@48646
  1065
    (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns));
wenzelm@48646
  1066
wenzelm@48646
  1067
val _ =
wenzelm@48646
  1068
  Outer_Syntax.command @{command_spec "extract_type"}
wenzelm@48646
  1069
    "add equations characterizing type of extracted program"
wenzelm@48646
  1070
    (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns));
wenzelm@48646
  1071
wenzelm@48646
  1072
val _ =
wenzelm@48646
  1073
  Outer_Syntax.command @{command_spec "extract"} "extract terms from proofs"
wenzelm@48646
  1074
    (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
wenzelm@48646
  1075
      Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
wenzelm@48646
  1076
wenzelm@48641
  1077
wenzelm@48641
  1078
wenzelm@48641
  1079
(** end **)
wenzelm@48641
  1080
wenzelm@48641
  1081
val _ =
wenzelm@48642
  1082
  Outer_Syntax.command @{command_spec "end"} "end context"
wenzelm@48641
  1083
    (Scan.succeed
wenzelm@48641
  1084
      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
wenzelm@48641
  1085
        Toplevel.end_proof (K Proof.end_notepad)));
wenzelm@48641
  1086
wenzelm@5832
  1087
end;
wenzelm@27614
  1088