src/Pure/Isar/isar_syn.ML
author wenzelm
Tue Mar 25 13:18:10 2014 +0100 (2014-03-25 ago)
changeset 56275 600f432ab556
parent 56240 938c6c7e10eb
child 56304 40274e4f5ebf
permissions -rw-r--r--
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
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@56275
   276
        in
wenzelm@56275
   277
          thy' |> Context.theory_map
wenzelm@56275
   278
            (ML_Context.exec (fn () => ML_Context.eval_source {SML = true, verbose = true} source))
wenzelm@56275
   279
        end)));
wenzelm@56275
   280
wenzelm@56275
   281
val _ =
wenzelm@48642
   282
  Outer_Syntax.command @{command_spec "ML"} "ML text within theory or local theory"
wenzelm@55828
   283
    (Parse.ML_source >> (fn source =>
wenzelm@30579
   284
      Toplevel.generic_theory
wenzelm@56275
   285
        (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source) #>
wenzelm@37949
   286
          Local_Theory.propagate_ml_env)));
wenzelm@30579
   287
wenzelm@30579
   288
val _ =
wenzelm@48642
   289
  Outer_Syntax.command @{command_spec "ML_prf"} "ML text within proof"
wenzelm@55828
   290
    (Parse.ML_source >> (fn source =>
wenzelm@28269
   291
      Toplevel.proof (Proof.map_context (Context.proof_map
wenzelm@56275
   292
        (ML_Context.exec (fn () => ML_Context.eval_source {SML = false, verbose = true} source))) #>
wenzelm@55828
   293
          Proof.propagate_ml_env)));
wenzelm@28269
   294
wenzelm@28269
   295
val _ =
wenzelm@48642
   296
  Outer_Syntax.command @{command_spec "ML_val"} "diagnostic ML text"
wenzelm@37216
   297
    (Parse.ML_source >> Isar_Cmd.ml_diag true);
wenzelm@26396
   298
wenzelm@26396
   299
val _ =
wenzelm@48642
   300
  Outer_Syntax.command @{command_spec "ML_command"} "diagnostic ML text (silent)"
wenzelm@51658
   301
    (Parse.ML_source >> Isar_Cmd.ml_diag false);
wenzelm@5832
   302
wenzelm@24868
   303
val _ =
wenzelm@48642
   304
  Outer_Syntax.command @{command_spec "setup"} "ML theory setup"
wenzelm@37216
   305
    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup));
wenzelm@30461
   306
wenzelm@30461
   307
val _ =
wenzelm@48642
   308
  Outer_Syntax.local_theory @{command_spec "local_setup"} "ML local theory setup"
wenzelm@37216
   309
    (Parse.ML_source >> Isar_Cmd.local_setup);
wenzelm@5832
   310
wenzelm@24868
   311
val _ =
wenzelm@48642
   312
  Outer_Syntax.command @{command_spec "attribute_setup"} "define attribute in ML"
wenzelm@42813
   313
    (Parse.position Parse.name --
wenzelm@48643
   314
        Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
wenzelm@36950
   315
      >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
wenzelm@30526
   316
wenzelm@30526
   317
val _ =
wenzelm@48642
   318
  Outer_Syntax.command @{command_spec "method_setup"} "define proof method in ML"
wenzelm@42813
   319
    (Parse.position Parse.name --
wenzelm@48643
   320
        Parse.!!! (@{keyword "="} |-- Parse.ML_source -- Scan.optional Parse.text "")
wenzelm@36950
   321
      >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
wenzelm@9197
   322
wenzelm@24868
   323
val _ =
wenzelm@48642
   324
  Outer_Syntax.local_theory @{command_spec "declaration"} "generic ML declaration"
wenzelm@40784
   325
    (Parse.opt_keyword "pervasive" -- Parse.ML_source
wenzelm@40784
   326
      >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
wenzelm@40784
   327
wenzelm@40784
   328
val _ =
wenzelm@48642
   329
  Outer_Syntax.local_theory @{command_spec "syntax_declaration"} "generic ML syntax declaration"
wenzelm@40784
   330
    (Parse.opt_keyword "pervasive" -- Parse.ML_source
wenzelm@40784
   331
      >> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
wenzelm@22088
   332
wenzelm@24868
   333
val _ =
wenzelm@48642
   334
  Outer_Syntax.local_theory @{command_spec "simproc_setup"} "define simproc in ML"
wenzelm@42464
   335
    (Parse.position Parse.name --
wenzelm@48643
   336
      (@{keyword "("} |-- Parse.enum1 "|" Parse.term --| @{keyword ")"} --| @{keyword "="}) --
wenzelm@48643
   337
      Parse.ML_source -- Scan.optional (@{keyword "identifier"} |-- Scan.repeat1 Parse.xname) []
wenzelm@37216
   338
    >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
wenzelm@22202
   339
wenzelm@5832
   340
wenzelm@5832
   341
(* translation functions *)
wenzelm@5832
   342
wenzelm@24868
   343
val _ =
wenzelm@48642
   344
  Outer_Syntax.command @{command_spec "parse_ast_translation"}
wenzelm@46961
   345
    "install parse ast translation functions"
wenzelm@52143
   346
    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
wenzelm@5832
   347
wenzelm@24868
   348
val _ =
wenzelm@48642
   349
  Outer_Syntax.command @{command_spec "parse_translation"}
wenzelm@46961
   350
    "install parse translation functions"
wenzelm@52143
   351
    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.parse_translation));
wenzelm@5832
   352
wenzelm@24868
   353
val _ =
wenzelm@48642
   354
  Outer_Syntax.command @{command_spec "print_translation"}
wenzelm@46961
   355
    "install print translation functions"
wenzelm@52143
   356
    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_translation));
wenzelm@5832
   357
wenzelm@24868
   358
val _ =
wenzelm@48642
   359
  Outer_Syntax.command @{command_spec "typed_print_translation"}
wenzelm@46961
   360
    "install typed print translation functions"
wenzelm@52143
   361
    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
wenzelm@5832
   362
wenzelm@24868
   363
val _ =
wenzelm@48642
   364
  Outer_Syntax.command @{command_spec "print_ast_translation"}
wenzelm@46961
   365
    "install print ast translation functions"
wenzelm@52143
   366
    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
wenzelm@5832
   367
wenzelm@5832
   368
wenzelm@5832
   369
(* oracles *)
wenzelm@5832
   370
wenzelm@24868
   371
val _ =
wenzelm@48642
   372
  Outer_Syntax.command @{command_spec "oracle"} "declare oracle"
wenzelm@48643
   373
    (Parse.position Parse.name -- (@{keyword "="} |-- Parse.ML_source) >>
wenzelm@37216
   374
      (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
wenzelm@5832
   375
wenzelm@5832
   376
wenzelm@47057
   377
(* bundled declarations *)
wenzelm@47057
   378
wenzelm@47057
   379
val _ =
wenzelm@48642
   380
  Outer_Syntax.local_theory @{command_spec "bundle"} "define bundle of declarations"
wenzelm@48643
   381
    ((Parse.binding --| @{keyword "="}) -- Parse_Spec.xthms1 -- Parse.for_fixes
wenzelm@47057
   382
      >> (uncurry Bundle.bundle_cmd));
wenzelm@47057
   383
wenzelm@47057
   384
val _ =
wenzelm@48642
   385
  Outer_Syntax.command @{command_spec "include"}
wenzelm@47057
   386
    "include declarations from bundle in proof body"
wenzelm@47066
   387
    (Scan.repeat1 (Parse.position Parse.xname)
wenzelm@47066
   388
      >> (Toplevel.print oo (Toplevel.proof o Bundle.include_cmd)));
wenzelm@47057
   389
wenzelm@47057
   390
val _ =
wenzelm@48642
   391
  Outer_Syntax.command @{command_spec "including"}
wenzelm@47057
   392
    "include declarations from bundle in goal refinement"
wenzelm@47066
   393
    (Scan.repeat1 (Parse.position Parse.xname)
wenzelm@47066
   394
      >> (Toplevel.print oo (Toplevel.proof o Bundle.including_cmd)));
wenzelm@47066
   395
wenzelm@47066
   396
val _ =
wenzelm@48642
   397
  Outer_Syntax.improper_command @{command_spec "print_bundles"}
wenzelm@48642
   398
    "print bundles of declarations"
wenzelm@51658
   399
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@47057
   400
      Toplevel.keep (Bundle.print_bundles o Toplevel.context_of)));
wenzelm@47057
   401
wenzelm@47057
   402
wenzelm@47069
   403
(* local theories *)
wenzelm@47069
   404
wenzelm@47069
   405
val _ =
wenzelm@48642
   406
  Outer_Syntax.command @{command_spec "context"} "begin local theory context"
wenzelm@47253
   407
    ((Parse.position Parse.xname >> (fn name =>
wenzelm@47253
   408
        Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)) ||
wenzelm@47253
   409
      Scan.optional Parse_Spec.includes [] -- Scan.repeat Parse_Spec.context_element
wenzelm@47253
   410
        >> (fn (incls, elems) => Toplevel.open_target (Bundle.context_cmd incls elems)))
wenzelm@47069
   411
      --| Parse.begin);
wenzelm@47069
   412
wenzelm@47069
   413
wenzelm@12061
   414
(* locales *)
wenzelm@12061
   415
wenzelm@12758
   416
val locale_val =
wenzelm@36952
   417
  Parse_Spec.locale_expression false --
wenzelm@48643
   418
    Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
wenzelm@36952
   419
  Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
wenzelm@12061
   420
wenzelm@24868
   421
val _ =
wenzelm@48642
   422
  Outer_Syntax.command @{command_spec "locale"} "define named proof context"
wenzelm@36950
   423
    (Parse.binding --
wenzelm@48643
   424
      Scan.optional (@{keyword "="} |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
haftmann@27681
   425
      >> (fn ((name, (expr, elems)), begin) =>
wenzelm@21843
   426
          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
wenzelm@41585
   427
            (Expression.add_locale_cmd I name Binding.empty expr elems #> snd)));
ballarin@28085
   428
wenzelm@53988
   429
fun interpretation_args mandatory =
ballarin@41270
   430
  Parse.!!! (Parse_Spec.locale_expression mandatory) --
ballarin@41270
   431
    Scan.optional
ballarin@41270
   432
      (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
ballarin@41270
   433
wenzelm@24868
   434
val _ =
wenzelm@48642
   435
  Outer_Syntax.command @{command_spec "sublocale"}
wenzelm@46961
   436
    "prove sublocale relation between a locale and a locale expression"
haftmann@51737
   437
    ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
wenzelm@53988
   438
      interpretation_args false >> (fn (loc, (expr, equations)) =>
wenzelm@53988
   439
        Toplevel.print o
wenzelm@53988
   440
        Toplevel.theory_to_proof (Expression.sublocale_global_cmd I loc expr equations)))
wenzelm@53988
   441
    || interpretation_args false >> (fn (expr, equations) =>
wenzelm@53988
   442
        Toplevel.print o
wenzelm@53988
   443
        Toplevel.local_theory_to_proof NONE (Expression.sublocale_cmd expr equations)));
ballarin@28895
   444
ballarin@28895
   445
val _ =
wenzelm@48642
   446
  Outer_Syntax.command @{command_spec "interpretation"}
haftmann@51737
   447
    "prove interpretation of locale expression in local theory"
wenzelm@53988
   448
    (interpretation_args true >> (fn (expr, equations) =>
wenzelm@53988
   449
      Toplevel.print o
wenzelm@53988
   450
      Toplevel.local_theory_to_proof NONE (Expression.interpretation_cmd expr equations)));
ballarin@29223
   451
ballarin@29223
   452
val _ =
wenzelm@48642
   453
  Outer_Syntax.command @{command_spec "interpret"}
ballarin@29223
   454
    "prove interpretation of locale expression in proof context"
wenzelm@53988
   455
    (interpretation_args true >> (fn (expr, equations) =>
wenzelm@53988
   456
      Toplevel.print o
wenzelm@53988
   457
      Toplevel.proof' (Expression.interpret_cmd expr equations)));
ballarin@29223
   458
wenzelm@15703
   459
haftmann@22299
   460
(* classes *)
haftmann@22299
   461
wenzelm@24868
   462
val class_val =
wenzelm@46922
   463
  Parse_Spec.class_expression --
wenzelm@48643
   464
    Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
wenzelm@36952
   465
  Scan.repeat1 Parse_Spec.context_element >> pair [];
haftmann@22299
   466
wenzelm@24868
   467
val _ =
wenzelm@48642
   468
  Outer_Syntax.command @{command_spec "class"} "define type class"
wenzelm@48643
   469
   (Parse.binding -- Scan.optional (@{keyword "="} |-- class_val) ([], []) -- Parse.opt_begin
haftmann@26516
   470
    >> (fn ((name, (supclasses, elems)), begin) =>
wenzelm@24938
   471
        (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
wenzelm@41585
   472
          (Class_Declaration.class_cmd I name supclasses elems #> snd)));
haftmann@22299
   473
wenzelm@24868
   474
val _ =
wenzelm@48642
   475
  Outer_Syntax.local_theory_to_proof @{command_spec "subclass"} "prove a subclass relation"
wenzelm@46922
   476
    (Parse.class >> Class_Declaration.subclass_cmd I);
haftmann@24914
   477
haftmann@24914
   478
val _ =
wenzelm@48642
   479
  Outer_Syntax.command @{command_spec "instantiation"} "instantiate and prove type arity"
wenzelm@36950
   480
   (Parse.multi_arity --| Parse.begin
haftmann@25462
   481
     >> (fn arities => Toplevel.print o
haftmann@38348
   482
         Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
haftmann@24589
   483
haftmann@25485
   484
val _ =
wenzelm@48642
   485
  Outer_Syntax.command @{command_spec "instance"} "prove type arity or subclass relation"
wenzelm@46922
   486
  ((Parse.class --
wenzelm@48643
   487
    ((@{keyword "\<subseteq>"} || @{keyword "<"}) |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
wenzelm@36950
   488
    Parse.multi_arity >> Class.instance_arity_cmd)
wenzelm@36950
   489
    >> (Toplevel.print oo Toplevel.theory_to_proof) ||
wenzelm@36950
   490
    Scan.succeed
wenzelm@36950
   491
      (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
haftmann@22299
   492
haftmann@22299
   493
haftmann@25519
   494
(* arbitrary overloading *)
haftmann@25519
   495
haftmann@25519
   496
val _ =
wenzelm@48642
   497
  Outer_Syntax.command @{command_spec "overloading"} "overloaded definitions"
wenzelm@48643
   498
   (Scan.repeat1 (Parse.name --| (@{keyword "\<equiv>"} || @{keyword "=="}) -- Parse.term --
wenzelm@48643
   499
      Scan.optional (@{keyword "("} |-- (@{keyword "unchecked"} >> K false) --| @{keyword ")"}) true
wenzelm@36950
   500
      >> Parse.triple1) --| Parse.begin
haftmann@25519
   501
   >> (fn operations => Toplevel.print o
haftmann@38342
   502
         Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
haftmann@25519
   503
haftmann@25519
   504
wenzelm@22866
   505
(* code generation *)
wenzelm@22866
   506
wenzelm@24868
   507
val _ =
wenzelm@48642
   508
  Outer_Syntax.command @{command_spec "code_datatype"}
wenzelm@46961
   509
    "define set of code datatype constructors"
wenzelm@36950
   510
    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
wenzelm@22866
   511
wenzelm@22866
   512
wenzelm@5832
   513
wenzelm@5832
   514
(** proof commands **)
wenzelm@5832
   515
wenzelm@5832
   516
(* statements *)
wenzelm@5832
   517
wenzelm@53988
   518
fun theorem spec schematic kind =
wenzelm@48645
   519
  Outer_Syntax.local_theory_to_proof' spec
wenzelm@36317
   520
    ("state " ^ (if schematic then "schematic " ^ kind else kind))
wenzelm@36952
   521
    (Scan.optional (Parse_Spec.opt_thm_name ":" --|
wenzelm@47067
   522
      Scan.ahead (Parse_Spec.includes >> K "" ||
wenzelm@47067
   523
        Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
wenzelm@47067
   524
      Scan.optional Parse_Spec.includes [] --
wenzelm@47067
   525
      Parse_Spec.general_statement >> (fn ((a, includes), (elems, concl)) =>
wenzelm@36317
   526
        ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
wenzelm@47067
   527
          kind NONE (K I) a includes elems concl)));
wenzelm@5832
   528
wenzelm@53988
   529
val _ = theorem @{command_spec "theorem"} false Thm.theoremK;
wenzelm@53988
   530
val _ = theorem @{command_spec "lemma"} false Thm.lemmaK;
wenzelm@53988
   531
val _ = theorem @{command_spec "corollary"} false Thm.corollaryK;
wenzelm@53988
   532
val _ = theorem @{command_spec "schematic_theorem"} true Thm.theoremK;
wenzelm@53988
   533
val _ = theorem @{command_spec "schematic_lemma"} true Thm.lemmaK;
wenzelm@53988
   534
val _ = theorem @{command_spec "schematic_corollary"} true Thm.corollaryK;
wenzelm@5832
   535
wenzelm@24868
   536
val _ =
wenzelm@48642
   537
  Outer_Syntax.local_theory_to_proof @{command_spec "notepad"} "begin proof context"
wenzelm@40960
   538
    (Parse.begin >> K Proof.begin_notepad);
wenzelm@40960
   539
wenzelm@40960
   540
val _ =
wenzelm@48642
   541
  Outer_Syntax.command @{command_spec "have"} "state local goal"
wenzelm@37216
   542
    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
wenzelm@17353
   543
wenzelm@24868
   544
val _ =
wenzelm@50214
   545
  Outer_Syntax.command @{command_spec "hence"} "old-style alias of \"then have\""
wenzelm@37216
   546
    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
wenzelm@17353
   547
wenzelm@24868
   548
val _ =
wenzelm@48642
   549
  Outer_Syntax.command @{command_spec "show"}
wenzelm@46961
   550
    "state local goal, solving current obligation"
wenzelm@37216
   551
    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
wenzelm@5832
   552
wenzelm@24868
   553
val _ =
wenzelm@50214
   554
  Outer_Syntax.command @{command_spec "thus"} "old-style alias of  \"then show\""
wenzelm@37216
   555
    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
wenzelm@6501
   556
wenzelm@5832
   557
wenzelm@5914
   558
(* facts *)
wenzelm@5832
   559
wenzelm@36952
   560
val facts = Parse.and_list1 Parse_Spec.xthms1;
wenzelm@9197
   561
wenzelm@24868
   562
val _ =
wenzelm@48642
   563
  Outer_Syntax.command @{command_spec "then"} "forward chaining"
wenzelm@17900
   564
    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
wenzelm@5832
   565
wenzelm@24868
   566
val _ =
wenzelm@48642
   567
  Outer_Syntax.command @{command_spec "from"} "forward chaining from given facts"
wenzelm@36323
   568
    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
wenzelm@5914
   569
wenzelm@24868
   570
val _ =
wenzelm@48642
   571
  Outer_Syntax.command @{command_spec "with"} "forward chaining from given and current facts"
wenzelm@36323
   572
    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
wenzelm@6878
   573
wenzelm@24868
   574
val _ =
wenzelm@48642
   575
  Outer_Syntax.command @{command_spec "note"} "define facts"
wenzelm@36952
   576
    (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
wenzelm@5832
   577
wenzelm@24868
   578
val _ =
wenzelm@48642
   579
  Outer_Syntax.command @{command_spec "using"} "augment goal facts"
wenzelm@36323
   580
    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
wenzelm@18544
   581
wenzelm@24868
   582
val _ =
wenzelm@48642
   583
  Outer_Syntax.command @{command_spec "unfolding"} "unfold definitions in goal and facts"
wenzelm@36323
   584
    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
wenzelm@12926
   585
wenzelm@5832
   586
wenzelm@5832
   587
(* proof context *)
wenzelm@5832
   588
wenzelm@24868
   589
val _ =
wenzelm@48642
   590
  Outer_Syntax.command @{command_spec "fix"} "fix local variables (Skolem constants)"
wenzelm@36950
   591
    (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
wenzelm@11890
   592
wenzelm@24868
   593
val _ =
wenzelm@48642
   594
  Outer_Syntax.command @{command_spec "assume"} "assume propositions"
wenzelm@36952
   595
    (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
wenzelm@5832
   596
wenzelm@24868
   597
val _ =
wenzelm@48642
   598
  Outer_Syntax.command @{command_spec "presume"} "assume propositions, to be established later"
wenzelm@36952
   599
    (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
wenzelm@6850
   600
wenzelm@24868
   601
val _ =
wenzelm@50214
   602
  Outer_Syntax.command @{command_spec "def"} "local definition (non-polymorphic)"
wenzelm@36950
   603
    (Parse.and_list1
wenzelm@36952
   604
      (Parse_Spec.opt_thm_name ":" --
wenzelm@36950
   605
        ((Parse.binding -- Parse.opt_mixfix) --
wenzelm@48643
   606
          ((@{keyword "\<equiv>"} || @{keyword "=="}) |-- Parse.!!! Parse.termp)))
wenzelm@36323
   607
    >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
wenzelm@6953
   608
wenzelm@24868
   609
val _ =
wenzelm@48642
   610
  Outer_Syntax.command @{command_spec "obtain"} "generalized elimination"
wenzelm@36952
   611
    (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
wenzelm@36323
   612
      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
wenzelm@5832
   613
wenzelm@24868
   614
val _ =
wenzelm@48642
   615
  Outer_Syntax.command @{command_spec "guess"} "wild guessing (unstructured)"
wenzelm@36950
   616
    (Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
wenzelm@17854
   617
wenzelm@24868
   618
val _ =
wenzelm@48642
   619
  Outer_Syntax.command @{command_spec "let"} "bind text variables"
wenzelm@48643
   620
    (Parse.and_list1 (Parse.and_list1 Parse.term -- (@{keyword "="} |-- Parse.term))
wenzelm@36323
   621
      >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
wenzelm@5832
   622
wenzelm@36505
   623
val _ =
wenzelm@48642
   624
  Outer_Syntax.command @{command_spec "write"} "add concrete syntax for constants / fixed variables"
wenzelm@51654
   625
    (opt_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
wenzelm@36505
   626
    >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
wenzelm@36505
   627
wenzelm@24868
   628
val _ =
wenzelm@48642
   629
  Outer_Syntax.command @{command_spec "case"} "invoke local context"
wenzelm@53377
   630
    ((@{keyword "("} |--
wenzelm@53378
   631
      Parse.!!! (Parse.position Parse.xname -- Scan.repeat (Parse.maybe Parse.binding)
wenzelm@53378
   632
        --| @{keyword ")"}) ||
wenzelm@53378
   633
      Parse.position Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> (fn ((c, xs), atts) =>
wenzelm@53377
   634
        Toplevel.print o Toplevel.proof (Proof.invoke_case_cmd (c, xs, atts))));
wenzelm@8370
   635
wenzelm@5832
   636
wenzelm@5832
   637
(* proof structure *)
wenzelm@5832
   638
wenzelm@24868
   639
val _ =
wenzelm@48642
   640
  Outer_Syntax.command @{command_spec "{"} "begin explicit proof block"
wenzelm@17900
   641
    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
wenzelm@5832
   642
wenzelm@24868
   643
val _ =
wenzelm@48642
   644
  Outer_Syntax.command @{command_spec "}"} "end explicit proof block"
wenzelm@20305
   645
    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
wenzelm@6687
   646
wenzelm@24868
   647
val _ =
wenzelm@48642
   648
  Outer_Syntax.command @{command_spec "next"} "enter next proof block"
wenzelm@17900
   649
    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
wenzelm@5832
   650
wenzelm@5832
   651
wenzelm@5832
   652
(* end proof *)
wenzelm@5832
   653
wenzelm@24868
   654
val _ =
wenzelm@50214
   655
  Outer_Syntax.command @{command_spec "qed"} "conclude proof"
wenzelm@55795
   656
    (Scan.option Method.parse >> (fn m => (Option.map Method.report m; Isar_Cmd.qed m)));
wenzelm@5832
   657
wenzelm@24868
   658
val _ =
wenzelm@48642
   659
  Outer_Syntax.command @{command_spec "by"} "terminal backward proof"
wenzelm@55795
   660
    (Method.parse -- Scan.option Method.parse >> (fn (m1, m2) =>
wenzelm@55795
   661
      (Method.report m1; Option.map Method.report m2; Isar_Cmd.terminal_proof (m1, m2))));
wenzelm@6404
   662
wenzelm@24868
   663
val _ =
wenzelm@48642
   664
  Outer_Syntax.command @{command_spec ".."} "default proof"
wenzelm@37216
   665
    (Scan.succeed Isar_Cmd.default_proof);
wenzelm@8966
   666
wenzelm@24868
   667
val _ =
wenzelm@48642
   668
  Outer_Syntax.command @{command_spec "."} "immediate proof"
wenzelm@37216
   669
    (Scan.succeed Isar_Cmd.immediate_proof);
wenzelm@6404
   670
wenzelm@24868
   671
val _ =
wenzelm@48642
   672
  Outer_Syntax.command @{command_spec "done"} "done proof"
wenzelm@37216
   673
    (Scan.succeed Isar_Cmd.done_proof);
wenzelm@5832
   674
wenzelm@24868
   675
val _ =
wenzelm@48642
   676
  Outer_Syntax.command @{command_spec "sorry"} "skip proof (quick-and-dirty mode only!)"
wenzelm@37216
   677
    (Scan.succeed Isar_Cmd.skip_proof);
wenzelm@6888
   678
wenzelm@24868
   679
val _ =
wenzelm@48642
   680
  Outer_Syntax.command @{command_spec "oops"} "forget proof"
wenzelm@18561
   681
    (Scan.succeed Toplevel.forget_proof);
wenzelm@8210
   682
wenzelm@5832
   683
wenzelm@5832
   684
(* proof steps *)
wenzelm@5832
   685
wenzelm@24868
   686
val _ =
wenzelm@48642
   687
  Outer_Syntax.command @{command_spec "defer"} "shuffle internal proof state"
wenzelm@49865
   688
    (Scan.optional Parse.nat 1 >> (fn n => Toplevel.print o Toplevel.proof (Proof.defer n)));
wenzelm@8165
   689
wenzelm@24868
   690
val _ =
wenzelm@48642
   691
  Outer_Syntax.command @{command_spec "prefer"} "shuffle internal proof state"
wenzelm@49865
   692
    (Parse.nat >> (fn n => Toplevel.print o Toplevel.proof (Proof.prefer n)));
wenzelm@8165
   693
wenzelm@24868
   694
val _ =
wenzelm@48642
   695
  Outer_Syntax.command @{command_spec "apply"} "initial refinement step (unstructured)"
wenzelm@55795
   696
    (Method.parse >> (fn m =>
wenzelm@55795
   697
      (Method.report m; Toplevel.print o Toplevel.proofs (Proof.apply_results m))));
wenzelm@5832
   698
wenzelm@24868
   699
val _ =
wenzelm@50214
   700
  Outer_Syntax.command @{command_spec "apply_end"} "terminal refinement step (unstructured)"
wenzelm@55795
   701
    (Method.parse >> (fn m =>
wenzelm@55795
   702
      (Method.report m; Toplevel.print o Toplevel.proofs (Proof.apply_end_results m))));
wenzelm@5832
   703
wenzelm@24868
   704
val _ =
wenzelm@50214
   705
  Outer_Syntax.command @{command_spec "proof"} "backward proof step"
wenzelm@55795
   706
    (Scan.option Method.parse >> (fn m =>
wenzelm@55795
   707
      (Option.map Method.report m;
wenzelm@55795
   708
        Toplevel.print o
wenzelm@55795
   709
        Toplevel.actual_proof (Proof_Node.applys (Proof.proof_results m)) o
wenzelm@55795
   710
        Toplevel.skip_proof (fn i => i + 1))));
wenzelm@5832
   711
wenzelm@5832
   712
wenzelm@6742
   713
(* proof navigation *)
wenzelm@5944
   714
wenzelm@56065
   715
fun report_back () =
wenzelm@56065
   716
  Output.report (Markup.markup Markup.bad "Explicit backtracking");
wenzelm@56065
   717
wenzelm@24868
   718
val _ =
wenzelm@56065
   719
  Outer_Syntax.command @{command_spec "back"} "explicit backtracking of proof command"
wenzelm@56065
   720
    (Scan.succeed (Toplevel.print o
wenzelm@56065
   721
      Toplevel.actual_proof (fn prf => (report_back (); Proof_Node.back prf)) o
wenzelm@56065
   722
      Toplevel.skip_proof (fn h => (report_back (); h))));
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@53988
   749
val _ = (*Proof General legacy*)
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@55997
   839
      Toplevel.keep (Attrib.print_attributes o Toplevel.context_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_methods"} "print methods of this theory"
wenzelm@51658
   854
    (Scan.succeed (Toplevel.unknown_theory o
wenzelm@55742
   855
      Toplevel.keep (Method.print_methods o Toplevel.context_of)));
wenzelm@5832
   856
wenzelm@24868
   857
val _ =
wenzelm@56069
   858
  Outer_Syntax.improper_command @{command_spec "print_antiquotations"}
wenzelm@56069
   859
    "print document antiquotations"
wenzelm@51658
   860
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@50737
   861
      Toplevel.keep (Thy_Output.print_antiquotations o Toplevel.context_of)));
wenzelm@9221
   862
wenzelm@24868
   863
val _ =
wenzelm@56069
   864
  Outer_Syntax.improper_command @{command_spec "print_ML_antiquotations"}
wenzelm@56069
   865
    "print ML antiquotations"
wenzelm@56069
   866
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@56069
   867
      Toplevel.keep (ML_Context.print_antiquotations o Toplevel.context_of)));
wenzelm@56069
   868
wenzelm@56069
   869
val _ =
wenzelm@48642
   870
  Outer_Syntax.improper_command @{command_spec "thy_deps"} "visualize theory dependencies"
wenzelm@51658
   871
    (Scan.succeed Isar_Cmd.thy_deps);
haftmann@22485
   872
wenzelm@24868
   873
val _ =
wenzelm@49569
   874
  Outer_Syntax.improper_command @{command_spec "locale_deps"} "visualize locale dependencies"
wenzelm@51658
   875
    (Scan.succeed Isar_Cmd.locale_deps);
wenzelm@49569
   876
wenzelm@49569
   877
val _ =
wenzelm@48642
   878
  Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
wenzelm@51658
   879
    (Scan.succeed Isar_Cmd.class_deps);
wenzelm@20574
   880
wenzelm@24868
   881
val _ =
wenzelm@48642
   882
  Outer_Syntax.improper_command @{command_spec "thm_deps"} "visualize theorem dependencies"
wenzelm@51658
   883
    (Parse_Spec.xthms1 >> Isar_Cmd.thm_deps);
wenzelm@9454
   884
wenzelm@24868
   885
val _ =
wenzelm@48642
   886
  Outer_Syntax.improper_command @{command_spec "print_binds"} "print term bindings of proof context"
wenzelm@51658
   887
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@50737
   888
      Toplevel.keep (Proof_Context.print_binds o Toplevel.context_of)));
wenzelm@5832
   889
wenzelm@24868
   890
val _ =
wenzelm@48642
   891
  Outer_Syntax.improper_command @{command_spec "print_facts"} "print facts of proof context"
wenzelm@56158
   892
    (opt_bang >> (fn verbose => Toplevel.unknown_context o
wenzelm@56158
   893
      Toplevel.keep (fn st => Proof_Context.print_local_facts (Toplevel.context_of st) verbose)));
wenzelm@5832
   894
wenzelm@24868
   895
val _ =
wenzelm@48642
   896
  Outer_Syntax.improper_command @{command_spec "print_cases"} "print cases of proof context"
wenzelm@51658
   897
    (Scan.succeed (Toplevel.unknown_context o
wenzelm@50737
   898
      Toplevel.keep (Proof_Context.print_cases o Toplevel.context_of)));
wenzelm@8370
   899
wenzelm@24868
   900
val _ =
wenzelm@48642
   901
  Outer_Syntax.improper_command @{command_spec "print_statement"}
wenzelm@46961
   902
    "print theorems as long statements"
wenzelm@51658
   903
    (opt_modes -- Parse_Spec.xthms1 >> Isar_Cmd.print_stmts);
wenzelm@19269
   904
wenzelm@24868
   905
val _ =
wenzelm@48642
   906
  Outer_Syntax.improper_command @{command_spec "thm"} "print theorems"
wenzelm@51658
   907
    (opt_modes -- Parse_Spec.xthms1 >> Isar_Cmd.print_thms);
wenzelm@5832
   908
wenzelm@24868
   909
val _ =
wenzelm@48642
   910
  Outer_Syntax.improper_command @{command_spec "prf"} "print proof terms of theorems"
wenzelm@51658
   911
    (opt_modes -- Scan.option Parse_Spec.xthms1 >> Isar_Cmd.print_prfs false);
berghofe@11524
   912
wenzelm@24868
   913
val _ =
wenzelm@48642
   914
  Outer_Syntax.improper_command @{command_spec "full_prf"} "print full proof terms of theorems"
wenzelm@51658
   915
    (opt_modes -- Scan.option Parse_Spec.xthms1 >> Isar_Cmd.print_prfs true);
berghofe@11524
   916
wenzelm@24868
   917
val _ =
wenzelm@48642
   918
  Outer_Syntax.improper_command @{command_spec "prop"} "read and print proposition"
wenzelm@51658
   919
    (opt_modes -- Parse.term >> Isar_Cmd.print_prop);
wenzelm@5832
   920
wenzelm@24868
   921
val _ =
wenzelm@48642
   922
  Outer_Syntax.improper_command @{command_spec "term"} "read and print term"
wenzelm@51658
   923
    (opt_modes -- Parse.term >> Isar_Cmd.print_term);
wenzelm@5832
   924
wenzelm@24868
   925
val _ =
wenzelm@48642
   926
  Outer_Syntax.improper_command @{command_spec "typ"} "read and print type"
wenzelm@48792
   927
    (opt_modes -- (Parse.typ -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort))
wenzelm@51658
   928
      >> Isar_Cmd.print_type);
wenzelm@5832
   929
wenzelm@24868
   930
val _ =
wenzelm@48642
   931
  Outer_Syntax.improper_command @{command_spec "print_codesetup"} "print code generator setup"
wenzelm@51658
   932
    (Scan.succeed (Toplevel.unknown_theory o
wenzelm@51658
   933
      Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
wenzelm@5832
   934
berghofe@26184
   935
val _ =
wenzelm@48642
   936
  Outer_Syntax.improper_command @{command_spec "unused_thms"} "find unused theorems"
wenzelm@36950
   937
    (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
wenzelm@51658
   938
       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >> Isar_Cmd.unused_thms);
berghofe@26184
   939
wenzelm@5832
   940
wenzelm@30142
   941
wenzelm@5832
   942
(** system commands (for interactive mode only) **)
wenzelm@5832
   943
wenzelm@24868
   944
val _ =
wenzelm@48642
   945
  Outer_Syntax.improper_command @{command_spec "cd"} "change current working directory"
wenzelm@51658
   946
    (Parse.path >> (fn name => Toplevel.imperative (fn () => File.cd (Path.explode name))));
wenzelm@5832
   947
wenzelm@24868
   948
val _ =
wenzelm@48642
   949
  Outer_Syntax.improper_command @{command_spec "pwd"} "print current working directory"
wenzelm@51658
   950
    (Scan.succeed (Toplevel.imperative (fn () => writeln (Path.print (File.pwd ())))));
wenzelm@5832
   951
wenzelm@24868
   952
val _ =
wenzelm@48642
   953
  Outer_Syntax.improper_command @{command_spec "use_thy"} "use theory file"
wenzelm@51658
   954
    (Parse.position Parse.name >>
wenzelm@51658
   955
      (fn name => Toplevel.imperative (fn () => Thy_Info.use_thy name)));
wenzelm@5832
   956
wenzelm@24868
   957
val _ =
wenzelm@48642
   958
  Outer_Syntax.improper_command @{command_spec "remove_thy"} "remove theory from loader database"
wenzelm@51658
   959
    (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
wenzelm@7102
   960
wenzelm@24868
   961
val _ =
wenzelm@48642
   962
  Outer_Syntax.improper_command @{command_spec "kill_thy"}
wenzelm@46961
   963
    "kill theory -- try to remove from loader database"
wenzelm@51658
   964
    (Parse.name >> (fn name => Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
wenzelm@7931
   965
wenzelm@53403
   966
val _ = (*partial Proof General legacy*)
wenzelm@48642
   967
  Outer_Syntax.improper_command @{command_spec "display_drafts"}
wenzelm@46961
   968
    "display raw source files with symbols"
wenzelm@52549
   969
    (Scan.repeat1 Parse.path >> (fn names =>
wenzelm@52549
   970
      Toplevel.imperative (fn () => ignore (Present.display_drafts (map Path.explode names)))));
wenzelm@14934
   971
wenzelm@52430
   972
val _ =
wenzelm@52430
   973
  Outer_Syntax.improper_command @{command_spec "print_state"}
wenzelm@52430
   974
    "print current proof state (if present)"
wenzelm@52430
   975
    (opt_modes >> (fn modes =>
wenzelm@52430
   976
      Toplevel.keep (fn state =>
wenzelm@52430
   977
        Print_Mode.with_modes modes (Toplevel.print_state true) state)));
wenzelm@52430
   978
wenzelm@53403
   979
val _ = (*Proof General legacy, e.g. for ProofGeneral-3.7.x*)
wenzelm@48642
   980
  Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
wenzelm@39165
   981
    (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
wenzelm@51658
   982
      Toplevel.keep (fn state =>
wenzelm@52438
   983
       (if Isabelle_Process.is_active () then error "Illegal TTY command" else ();
wenzelm@52438
   984
        case limit of NONE => () | SOME n => Options.default_put_int @{option goals_limit} n;
wenzelm@39165
   985
        Toplevel.quiet := false;
wenzelm@39165
   986
        Print_Mode.with_modes modes (Toplevel.print_state true) state))));
wenzelm@7199
   987
wenzelm@53403
   988
val _ = (*Proof General legacy*)
wenzelm@48642
   989
  Outer_Syntax.improper_command @{command_spec "disable_pr"}
wenzelm@46961
   990
    "disable printing of toplevel state"
wenzelm@51658
   991
    (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := true)));
wenzelm@5832
   992
wenzelm@53403
   993
val _ = (*Proof General legacy*)
wenzelm@48642
   994
  Outer_Syntax.improper_command @{command_spec "enable_pr"}
wenzelm@46961
   995
    "enable printing of toplevel state"
wenzelm@51658
   996
    (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := false)));
wenzelm@7222
   997
wenzelm@24868
   998
val _ =
wenzelm@48642
   999
  Outer_Syntax.improper_command @{command_spec "commit"}
wenzelm@50214
  1000
    "commit current session to ML session image"
wenzelm@51658
  1001
    (Parse.opt_unit >> K (Toplevel.imperative Secure.commit));
wenzelm@5832
  1002
wenzelm@24868
  1003
val _ =
wenzelm@48642
  1004
  Outer_Syntax.improper_command @{command_spec "quit"} "quit Isabelle"
wenzelm@51658
  1005
    (Parse.opt_unit >> (K (Toplevel.imperative quit)));
wenzelm@5832
  1006
wenzelm@24868
  1007
val _ =
wenzelm@48642
  1008
  Outer_Syntax.improper_command @{command_spec "exit"} "exit Isar loop"
wenzelm@37977
  1009
    (Scan.succeed
wenzelm@51658
  1010
      (Toplevel.keep (fn state =>
wenzelm@37977
  1011
        (Context.set_thread_data (try Toplevel.generic_theory_of state);
wenzelm@38888
  1012
          raise Runtime.TERMINATE))));
wenzelm@5832
  1013
wenzelm@48646
  1014
val _ =
wenzelm@48646
  1015
  Outer_Syntax.improper_command @{command_spec "welcome"} "print welcome message"
wenzelm@51658
  1016
    (Scan.succeed (Toplevel.imperative (writeln o Session.welcome)));
wenzelm@48646
  1017
wenzelm@48646
  1018
wenzelm@48646
  1019
wenzelm@48646
  1020
(** raw Isar read-eval-print loop **)
wenzelm@48646
  1021
wenzelm@48646
  1022
val _ =
wenzelm@48646
  1023
  Outer_Syntax.improper_command @{command_spec "init_toplevel"} "init toplevel point-of-interest"
wenzelm@51658
  1024
    (Scan.succeed (Toplevel.imperative Isar.init));
wenzelm@48646
  1025
wenzelm@48646
  1026
val _ =
wenzelm@48646
  1027
  Outer_Syntax.improper_command @{command_spec "linear_undo"} "undo commands"
wenzelm@48646
  1028
    (Scan.optional Parse.nat 1 >>
wenzelm@51658
  1029
      (fn n => Toplevel.imperative (fn () => Isar.linear_undo n)));
wenzelm@48646
  1030
wenzelm@48646
  1031
val _ =
wenzelm@48646
  1032
  Outer_Syntax.improper_command @{command_spec "undo"} "undo commands (skipping closed proofs)"
wenzelm@48646
  1033
    (Scan.optional Parse.nat 1 >>
wenzelm@51658
  1034
      (fn n => Toplevel.imperative (fn () => Isar.undo n)));
wenzelm@48646
  1035
wenzelm@48646
  1036
val _ =
wenzelm@48646
  1037
  Outer_Syntax.improper_command @{command_spec "undos_proof"}
wenzelm@48646
  1038
    "undo commands (skipping closed proofs)"
wenzelm@51658
  1039
    (Scan.optional Parse.nat 1 >> (fn n =>
wenzelm@48646
  1040
      Toplevel.keep (fn state =>
wenzelm@48646
  1041
        if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF)));
wenzelm@48646
  1042
wenzelm@48646
  1043
val _ =
wenzelm@48646
  1044
  Outer_Syntax.improper_command @{command_spec "cannot_undo"}
wenzelm@48646
  1045
    "partial undo -- Proof General legacy"
wenzelm@48646
  1046
    (Parse.name >>
wenzelm@51658
  1047
      (fn "end" => Toplevel.imperative (fn () => Isar.undo 1)
wenzelm@48646
  1048
        | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
wenzelm@48646
  1049
wenzelm@48646
  1050
val _ =
wenzelm@48646
  1051
  Outer_Syntax.improper_command @{command_spec "kill"}
wenzelm@48646
  1052
    "kill partial proof or theory development"
wenzelm@51658
  1053
    (Scan.succeed (Toplevel.imperative Isar.kill));
wenzelm@48646
  1054
wenzelm@48646
  1055
wenzelm@48646
  1056
wenzelm@48646
  1057
(** extraction of programs from proofs **)
wenzelm@48646
  1058
wenzelm@48646
  1059
val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
wenzelm@48646
  1060
wenzelm@48646
  1061
val _ =
wenzelm@48646
  1062
  Outer_Syntax.command @{command_spec "realizers"}
wenzelm@48646
  1063
    "specify realizers for primitive axioms / theorems, together with correctness proof"
wenzelm@48646
  1064
    (Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
wenzelm@48646
  1065
     (fn xs => Toplevel.theory (fn thy => Extraction.add_realizers
wenzelm@48646
  1066
       (map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
wenzelm@48646
  1067
wenzelm@48646
  1068
val _ =
wenzelm@48646
  1069
  Outer_Syntax.command @{command_spec "realizability"}
wenzelm@48646
  1070
    "add equations characterizing realizability"
wenzelm@48646
  1071
    (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_realizes_eqns));
wenzelm@48646
  1072
wenzelm@48646
  1073
val _ =
wenzelm@48646
  1074
  Outer_Syntax.command @{command_spec "extract_type"}
wenzelm@48646
  1075
    "add equations characterizing type of extracted program"
wenzelm@48646
  1076
    (Scan.repeat1 Parse.string >> (Toplevel.theory o Extraction.add_typeof_eqns));
wenzelm@48646
  1077
wenzelm@48646
  1078
val _ =
wenzelm@48646
  1079
  Outer_Syntax.command @{command_spec "extract"} "extract terms from proofs"
wenzelm@48646
  1080
    (Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
wenzelm@48646
  1081
      Extraction.extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
wenzelm@48646
  1082
wenzelm@48641
  1083
wenzelm@48641
  1084
wenzelm@48641
  1085
(** end **)
wenzelm@48641
  1086
wenzelm@48641
  1087
val _ =
wenzelm@48642
  1088
  Outer_Syntax.command @{command_spec "end"} "end context"
wenzelm@48641
  1089
    (Scan.succeed
wenzelm@48641
  1090
      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.close_target o
wenzelm@48641
  1091
        Toplevel.end_proof (K Proof.end_notepad)));
wenzelm@48641
  1092
wenzelm@5832
  1093
end;
wenzelm@27614
  1094