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