src/Pure/Isar/isar_syn.ML
author wenzelm
Tue, 31 Aug 2010 23:46:49 +0200
changeset 38888 8248cda328de
parent 38870 fb9f51ba1bbc
child 39165 e790a5560834
permissions -rw-r--r--
moved Toplevel.run_command to Pure/PIDE/document.ML; eliminated aliases of exception Toplevel.TERMINATE and Toplevel.EXCURSION_FAIL; tuned signatures;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/isar_syn.ML
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
     2
    Author:     Markus Wenzel, TU Muenchen
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
     3
6353
5a76eb9030df added 'title';
wenzelm
parents: 6265
diff changeset
     4
Isar/Pure outer syntax.
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
     5
*)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
     6
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
     7
structure Isar_Syn: sig end =
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
     8
struct
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
     9
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    10
(** keywords **)
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    11
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    12
(*keep keywords consistent with the parsers, otherwise be prepared for
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    13
  unexpected errors*)
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    14
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
    15
val _ = List.app Keyword.keyword
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    16
 ["!!", "!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    17
  "=", "==", "=>", "?", "[", "\\<equiv>", "\\<leftharpoondown>",
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    18
  "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
26888
9942cd184c48 remobed obsolete keyword concl;
wenzelm
parents: 26676
diff changeset
    19
  "advanced", "and", "assumes", "attach", "begin", "binder",
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    20
  "constrains", "defines", "fixes", "for", "identifier", "if",
28721
21170e10c745 Keyword 'includes' gone.
ballarin
parents: 28301
diff changeset
    21
  "imports", "in", "infix", "infixl", "infixr", "is",
33456
fbd47f9b9b12 allow "pervasive" local theory declarations, which are applied the background theory;
wenzelm
parents: 33390
diff changeset
    22
  "notes", "obtains", "open", "output", "overloaded", "pervasive",
fbd47f9b9b12 allow "pervasive" local theory declarations, which are applied the background theory;
wenzelm
parents: 33390
diff changeset
    23
  "shows", "structure", "unchecked", "uses", "where", "|"];
fbd47f9b9b12 allow "pervasive" local theory declarations, which are applied the background theory;
wenzelm
parents: 33390
diff changeset
    24
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    25
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    26
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
    27
(** init and exit **)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
    28
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    29
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
    30
  Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
37977
3ceccd415145 simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents: 37949
diff changeset
    31
    (Thy_Header.args >> (fn (name, imports, uses) =>
3ceccd415145 simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents: 37949
diff changeset
    32
      Toplevel.print o
3ceccd415145 simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents: 37949
diff changeset
    33
        Toplevel.init_theory name
3ceccd415145 simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents: 37949
diff changeset
    34
          (fn () => Thy_Info.toplevel_begin_theory name imports (map (apfst Path.explode) uses))));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
    35
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    36
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
    37
  Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
21004
wenzelm
parents: 20979
diff changeset
    38
    (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
6687
134df1440f6e renamed 'begin' / 'end' to '{{' / '}}';
wenzelm
parents: 6551
diff changeset
    39
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
    40
30142
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29882
diff changeset
    41
7749
dfb8beddbefe OuterSyntax.markup_command;
wenzelm
parents: 7733
diff changeset
    42
(** markup commands **)
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
    43
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    44
val _ = Outer_Syntax.markup_command Thy_Output.Markup "header" "theory header" Keyword.diag
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    45
  (Parse.doc_source >> Isar_Cmd.header_markup);
6353
5a76eb9030df added 'title';
wenzelm
parents: 6265
diff changeset
    46
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    47
val _ = Outer_Syntax.markup_command Thy_Output.Markup "chapter" "chapter heading"
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    48
  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
5958
c48efb523a4d chapter etc. headings;
wenzelm
parents: 5944
diff changeset
    49
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    50
val _ = Outer_Syntax.markup_command Thy_Output.Markup "section" "section heading"
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    51
  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
5958
c48efb523a4d chapter etc. headings;
wenzelm
parents: 5944
diff changeset
    52
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    53
val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsection" "subsection heading"
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    54
  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
5958
c48efb523a4d chapter etc. headings;
wenzelm
parents: 5944
diff changeset
    55
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    56
val _ =
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    57
  Outer_Syntax.markup_command Thy_Output.Markup "subsubsection" "subsubsection heading"
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    58
  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
    59
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    60
val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "text" "formal comment (theory)"
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    61
  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
7172
wenzelm
parents: 7140
diff changeset
    62
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    63
val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "text_raw" "raw document preparation text"
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    64
  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
7172
wenzelm
parents: 7140
diff changeset
    65
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    66
val _ = Outer_Syntax.markup_command Thy_Output.Markup "sect" "formal comment (proof)"
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    67
  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
7172
wenzelm
parents: 7140
diff changeset
    68
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    69
val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsect" "formal comment (proof)"
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    70
  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
7172
wenzelm
parents: 7140
diff changeset
    71
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    72
val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsubsect" "formal comment (proof)"
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    73
  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
7172
wenzelm
parents: 7140
diff changeset
    74
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    75
val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "txt" "formal comment (proof)"
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    76
  (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> Isar_Cmd.proof_markup);
7172
wenzelm
parents: 7140
diff changeset
    77
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    78
val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "txt_raw"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
    79
  "raw document preparation text (proof)" (Keyword.tag_proof Keyword.prf_decl)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
    80
  (Parse.doc_source >> Isar_Cmd.proof_markup);
7775
26898fbd19ca verbatim / verb markupup commands;
wenzelm
parents: 7749
diff changeset
    81
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
    82
6886
7d0f7ad5a35f added 'txt';
wenzelm
parents: 6878
diff changeset
    83
30142
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29882
diff changeset
    84
(** theory commands **)
6886
7d0f7ad5a35f added 'txt';
wenzelm
parents: 6878
diff changeset
    85
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
    86
(* classes and sorts *)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
    87
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    88
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
    89
  Outer_Syntax.command "classes" "declare type classes" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
    90
    (Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |--
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
    91
        Parse.!!! (Parse.list1 Parse.xname)) [])
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
    92
      >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
    93
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
    94
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
    95
  Outer_Syntax.command "classrel" "state inclusion of type classes (axiomatic!)" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
    96
    (Parse.and_list1 (Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
    97
        |-- Parse.!!! Parse.xname))
24932
86ef9a828a9e AxClass.axiomatize and Specification: renamed XXX_i to XXX, and XXX to XXX_cmd;
wenzelm
parents: 24914
diff changeset
    98
    >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
    99
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   100
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   101
  Outer_Syntax.local_theory "default_sort" "declare default sort for explicit type variables"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   102
    Keyword.thy_decl
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   103
    (Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   104
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   105
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   106
(* types *)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   107
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   108
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   109
  Outer_Syntax.local_theory "typedecl" "type declaration" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   110
    (Parse.type_args -- Parse.binding -- Parse.opt_mixfix
35835
51c6ac100bd9 typedecl: no sort constraints;
wenzelm
parents: 35681
diff changeset
   111
      >> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   112
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   113
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   114
  Outer_Syntax.local_theory "types" "declare type abbreviations" Keyword.thy_decl
6727
c8dba1da73cc renamed Comment.empty to Comment.none;
wenzelm
parents: 6723
diff changeset
   115
    (Scan.repeat1
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   116
      (Parse.type_args -- Parse.binding --
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   117
        (Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix')))
36178
0e5c133b48b6 keep localized 'types' as regular non-old-style version -- 'type_abbrev' as 'type' just causes too many problems, e.g. clash with "type" in translations or "type:" argument syntax;
wenzelm
parents: 36176
diff changeset
   118
      >> (fold (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs)));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   119
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   120
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   121
  Outer_Syntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   122
    Keyword.thy_decl (Scan.repeat1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   123
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   124
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   125
  Outer_Syntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   126
    (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   127
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   128
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   129
(* consts and syntax *)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   130
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   131
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   132
  Outer_Syntax.command "judgment" "declare object-logic judgment" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   133
    (Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
8227
d67db92897df add_judgment;
wenzelm
parents: 8210
diff changeset
   134
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   135
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   136
  Outer_Syntax.command "consts" "declare constants" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   137
    (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   138
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   139
val opt_overloaded = Parse.opt_keyword "overloaded";
14223
0ee05eef881b Added support for making constants final, that is, ensuring that no
skalberg
parents: 13802
diff changeset
   140
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   141
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   142
  Outer_Syntax.command "finalconsts" "declare constants as final" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   143
    (opt_overloaded -- Scan.repeat1 Parse.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
9731
3eb72671e5db pr: added prems limit;
wenzelm
parents: 9589
diff changeset
   144
12142
c81ef8865cfb "theorem" etc.: multiple statements;
wenzelm
parents: 12125
diff changeset
   145
val mode_spec =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   146
  (Parse.$$$ "output" >> K ("", false)) ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   147
    Parse.name -- Scan.optional (Parse.$$$ "output" >> K false) true;
9731
3eb72671e5db pr: added prems limit;
wenzelm
parents: 9589
diff changeset
   148
14900
c66394c408f7 Syntax.default_mode;
wenzelm
parents: 14779
diff changeset
   149
val opt_mode =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   150
  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (mode_spec --| Parse.$$$ ")")) Syntax.mode_default;
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   151
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   152
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   153
  Outer_Syntax.command "syntax" "declare syntactic constants" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   154
    (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.add_modesyntax));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   155
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   156
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   157
  Outer_Syntax.command "no_syntax" "delete syntax declarations" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   158
    (opt_mode -- Scan.repeat1 Parse.const >> (Toplevel.theory o uncurry Sign.del_modesyntax));
15748
e26fdd4aa95a added 'no_syntax' command;
wenzelm
parents: 15712
diff changeset
   159
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   160
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   161
(* translations *)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   162
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   163
val trans_pat =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   164
  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.xname --| Parse.$$$ ")")) "logic"
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   165
    -- Parse.string;
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   166
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   167
fun trans_arrow toks =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   168
  ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.ParseRule ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   169
    (Parse.$$$ "\\<leftharpoondown>" || Parse.$$$ "<=") >> K Syntax.PrintRule ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   170
    (Parse.$$$ "\\<rightleftharpoons>" || Parse.$$$ "==") >> K Syntax.ParsePrintRule) toks;
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   171
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   172
val trans_line =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   173
  trans_pat -- Parse.!!! (trans_arrow -- trans_pat)
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   174
    >> (fn (left, (arr, right)) => arr (left, right));
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   175
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   176
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   177
  Outer_Syntax.command "translations" "declare syntax translation rules" Keyword.thy_decl
22796
34c316d7b630 renamed some old names Theory.xxx to Sign.xxx;
wenzelm
parents: 22744
diff changeset
   178
    (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.add_trrules));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   179
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   180
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   181
  Outer_Syntax.command "no_translations" "remove syntax translation rules" Keyword.thy_decl
22796
34c316d7b630 renamed some old names Theory.xxx to Sign.xxx;
wenzelm
parents: 22744
diff changeset
   182
    (Scan.repeat1 trans_line >> (Toplevel.theory o Sign.del_trrules));
19260
a3d3a4b75c71 added 'no_translations';
wenzelm
parents: 19245
diff changeset
   183
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   184
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   185
(* axioms and definitions *)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   186
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   187
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   188
  Outer_Syntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   189
    (Scan.repeat1 Parse_Spec.spec >>
37861
e1f028a8c76a warning in proper transaction context;
wenzelm
parents: 37216
diff changeset
   190
      (fn spec => Toplevel.theory (fn thy =>
e1f028a8c76a warning in proper transaction context;
wenzelm
parents: 37216
diff changeset
   191
        (legacy_feature "Old 'axioms' command -- use 'axiomatization' instead";
e1f028a8c76a warning in proper transaction context;
wenzelm
parents: 37216
diff changeset
   192
          Isar_Cmd.add_axioms spec thy))));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   193
19631
4445b353f78b 'defs': unchecked flag;
wenzelm
parents: 19516
diff changeset
   194
val opt_unchecked_overloaded =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   195
  Scan.optional (Parse.$$$ "(" |-- Parse.!!!
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   196
    (((Parse.$$$ "unchecked" >> K true) -- Scan.optional (Parse.$$$ "overloaded" >> K true) false ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   197
      Parse.$$$ "overloaded" >> K (false, true)) --| Parse.$$$ ")")) (false, false);
19631
4445b353f78b 'defs': unchecked flag;
wenzelm
parents: 19516
diff changeset
   198
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   199
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   200
  Outer_Syntax.command "defs" "define constants" Keyword.thy_decl
35852
4e3fe0b8687b minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';
wenzelm
parents: 35835
diff changeset
   201
    (opt_unchecked_overloaded --
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   202
      Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   203
      >> (Toplevel.theory o Isar_Cmd.add_defs));
6370
e71ac23a9111 OuterSyntax.(improper_)command;
wenzelm
parents: 6353
diff changeset
   204
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14528
diff changeset
   205
21601
6588b947d631 simplified syntax for 'definition', 'abbreviation';
wenzelm
parents: 21527
diff changeset
   206
(* old constdefs *)
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14528
diff changeset
   207
21601
6588b947d631 simplified syntax for 'definition', 'abbreviation';
wenzelm
parents: 21527
diff changeset
   208
val old_constdecl =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   209
  Parse.binding --| Parse.where_ >> (fn x => (x, NONE, NoSyn)) ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   210
  Parse.binding -- (Parse.$$$ "::" |-- Parse.!!! Parse.typ >> SOME) -- Parse.opt_mixfix'
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   211
    --| Scan.option Parse.where_ >> Parse.triple1 ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   212
  Parse.binding -- (Parse.mixfix >> pair NONE) --| Scan.option Parse.where_ >> Parse.triple2;
19076
e1948ebe9c7d added 'abbreviation';
wenzelm
parents: 18949
diff changeset
   213
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   214
val old_constdef = Scan.option old_constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop);
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14528
diff changeset
   215
19076
e1948ebe9c7d added 'abbreviation';
wenzelm
parents: 18949
diff changeset
   216
val structs =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   217
  Scan.optional ((Parse.$$$ "(" -- Parse.$$$ "structure")
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   218
    |-- Parse.!!! (Parse.simple_fixes --| Parse.$$$ ")")) [];
19076
e1948ebe9c7d added 'abbreviation';
wenzelm
parents: 18949
diff changeset
   219
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   220
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   221
  Outer_Syntax.command "constdefs" "old-style constant definition" Keyword.thy_decl
21601
6588b947d631 simplified syntax for 'definition', 'abbreviation';
wenzelm
parents: 21527
diff changeset
   222
    (structs -- Scan.repeat1 old_constdef >> (Toplevel.theory o Constdefs.add_constdefs));
6588b947d631 simplified syntax for 'definition', 'abbreviation';
wenzelm
parents: 21527
diff changeset
   223
6588b947d631 simplified syntax for 'definition', 'abbreviation';
wenzelm
parents: 21527
diff changeset
   224
6588b947d631 simplified syntax for 'definition', 'abbreviation';
wenzelm
parents: 21527
diff changeset
   225
(* constant definitions and abbreviations *)
6588b947d631 simplified syntax for 'definition', 'abbreviation';
wenzelm
parents: 21527
diff changeset
   226
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   227
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   228
  Outer_Syntax.local_theory "definition" "constant definition" Keyword.thy_decl
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   229
    (Parse_Spec.constdef >> (fn args => #2 o Specification.definition_cmd args));
18780
a9c38d41cd27 added 'definition';
wenzelm
parents: 18766
diff changeset
   230
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   231
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   232
  Outer_Syntax.local_theory "abbreviation" "constant abbreviation" Keyword.thy_decl
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   233
    (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   234
      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
19659
88d246e5f4bd added 'const_syntax';
wenzelm
parents: 19631
diff changeset
   235
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   236
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   237
  Outer_Syntax.local_theory "type_notation" "add concrete syntax for type constructors"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   238
    Keyword.thy_decl
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   239
    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   240
      >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
35413
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   241
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   242
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   243
  Outer_Syntax.local_theory "no_type_notation" "delete concrete syntax for type constructors"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   244
    Keyword.thy_decl
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   245
    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse.mixfix)
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   246
      >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
35413
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   247
4c7cba1f7ce9 added type_notation command;
wenzelm
parents: 35351
diff changeset
   248
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   249
  Outer_Syntax.local_theory "notation" "add concrete syntax for constants / fixed variables"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   250
    Keyword.thy_decl
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   251
    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   252
      >> (fn (mode, args) => Specification.notation_cmd true mode args));
24950
106fc30769a9 added 'no_notation';
wenzelm
parents: 24938
diff changeset
   253
106fc30769a9 added 'no_notation';
wenzelm
parents: 24938
diff changeset
   254
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   255
  Outer_Syntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   256
    Keyword.thy_decl
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   257
    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   258
      >> (fn (mode, args) => Specification.notation_cmd false mode args));
19076
e1948ebe9c7d added 'abbreviation';
wenzelm
parents: 18949
diff changeset
   259
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   260
18616
cf5d07758d3f added 'axiomatization';
wenzelm
parents: 18561
diff changeset
   261
(* constant specifications *)
cf5d07758d3f added 'axiomatization';
wenzelm
parents: 18561
diff changeset
   262
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   263
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   264
  Outer_Syntax.command "axiomatization" "axiomatic constant specification" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   265
    (Scan.optional Parse.fixes [] --
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   266
      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   267
      >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
18616
cf5d07758d3f added 'axiomatization';
wenzelm
parents: 18561
diff changeset
   268
cf5d07758d3f added 'axiomatization';
wenzelm
parents: 18561
diff changeset
   269
5914
2c069b0a98ee added 'theorems', 'lemmas', 'note';
wenzelm
parents: 5896
diff changeset
   270
(* theorems *)
2c069b0a98ee added 'theorems', 'lemmas', 'note';
wenzelm
parents: 5896
diff changeset
   271
26988
742e26213212 more uniform treatment of OuterSyntax.local_theory commands;
wenzelm
parents: 26888
diff changeset
   272
fun theorems kind =
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   273
  Parse_Spec.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args);
12712
a659fd913a89 localized 'lemmas', 'theorems', 'declare';
wenzelm
parents: 12696
diff changeset
   274
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   275
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   276
  Outer_Syntax.local_theory "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
5914
2c069b0a98ee added 'theorems', 'lemmas', 'note';
wenzelm
parents: 5896
diff changeset
   277
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   278
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   279
  Outer_Syntax.local_theory "lemmas" "define lemmas" Keyword.thy_decl (theorems Thm.lemmaK);
5914
2c069b0a98ee added 'theorems', 'lemmas', 'note';
wenzelm
parents: 5896
diff changeset
   280
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   281
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   282
  Outer_Syntax.local_theory "declare" "declare theorems" Keyword.thy_decl
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   283
    (Parse.and_list1 Parse_Spec.xthms1
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28951
diff changeset
   284
      >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
9589
95a66548c883 added "declare" command;
wenzelm
parents: 9552
diff changeset
   285
5914
2c069b0a98ee added 'theorems', 'lemmas', 'note';
wenzelm
parents: 5896
diff changeset
   286
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   287
(* name space entry path *)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   288
36176
3fe7e97ccca8 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents: 36174
diff changeset
   289
fun hide_names name hide what =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   290
  Outer_Syntax.command name ("hide " ^ what ^ " from name space") Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   291
    ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
36176
3fe7e97ccca8 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents: 36174
diff changeset
   292
      (Toplevel.theory o uncurry hide));
3fe7e97ccca8 replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents: 36174
diff changeset
   293
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   294
val _ = hide_names "hide_class" Isar_Cmd.hide_class "classes";
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   295
val _ = hide_names "hide_type" Isar_Cmd.hide_type "types";
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   296
val _ = hide_names "hide_const" Isar_Cmd.hide_const "constants";
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   297
val _ = hide_names "hide_fact" Isar_Cmd.hide_fact "facts";
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   298
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   299
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   300
(* use ML text *)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   301
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   302
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   303
  Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
37949
48a874444164 moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents: 37873
diff changeset
   304
    (Parse.path >> (fn path => Toplevel.generic_theory (Thy_Load.exec_ml path)));
7891
c77ad0c3c92f use_mltext: better control of verbosity;
wenzelm
parents: 7885
diff changeset
   305
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   306
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   307
  Outer_Syntax.command "ML" "ML text within theory or local theory"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   308
    (Keyword.tag_ml Keyword.thy_decl)
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   309
    (Parse.ML_source >> (fn (txt, pos) =>
30579
4169ddbfe1f9 command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents: 30576
diff changeset
   310
      Toplevel.generic_theory
37949
48a874444164 moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents: 37873
diff changeset
   311
        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
48a874444164 moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents: 37873
diff changeset
   312
          Local_Theory.propagate_ml_env)));
30579
4169ddbfe1f9 command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents: 30576
diff changeset
   313
4169ddbfe1f9 command 'use', 'ML': apply ML environment to theory and target as well;
wenzelm
parents: 30576
diff changeset
   314
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   315
  Outer_Syntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   316
    (Parse.ML_source >> (fn (txt, pos) =>
28269
b1e5e6c4c10e added ML_prf;
wenzelm
parents: 28259
diff changeset
   317
      Toplevel.proof (Proof.map_context (Context.proof_map
37949
48a874444164 moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
wenzelm
parents: 37873
diff changeset
   318
        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));
28269
b1e5e6c4c10e added ML_prf;
wenzelm
parents: 28259
diff changeset
   319
b1e5e6c4c10e added ML_prf;
wenzelm
parents: 28259
diff changeset
   320
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   321
  Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   322
    (Parse.ML_source >> Isar_Cmd.ml_diag true);
26396
e44c5a1a47bd added 'ML_val' command (diagnostic);
wenzelm
parents: 26385
diff changeset
   323
e44c5a1a47bd added 'ML_val' command (diagnostic);
wenzelm
parents: 26385
diff changeset
   324
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   325
  Outer_Syntax.command "ML_command" "diagnostic ML text (silent)" (Keyword.tag_ml Keyword.diag)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   326
    (Parse.ML_source >> (Toplevel.no_timing oo Isar_Cmd.ml_diag false));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   327
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   328
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   329
  Outer_Syntax.command "setup" "ML theory setup" (Keyword.tag_ml Keyword.thy_decl)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   330
    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup));
30461
00323c45ea83 added 'local_setup' command;
wenzelm
parents: 30344
diff changeset
   331
00323c45ea83 added 'local_setup' command;
wenzelm
parents: 30344
diff changeset
   332
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   333
  Outer_Syntax.local_theory "local_setup" "ML local theory setup" (Keyword.tag_ml Keyword.thy_decl)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   334
    (Parse.ML_source >> Isar_Cmd.local_setup);
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   335
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   336
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   337
  Outer_Syntax.command "attribute_setup" "define attribute in ML" (Keyword.tag_ml Keyword.thy_decl)
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   338
    (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text)
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   339
      >> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
30526
7f9a9ec1c94d added 'attribute_setup' command;
wenzelm
parents: 30484
diff changeset
   340
7f9a9ec1c94d added 'attribute_setup' command;
wenzelm
parents: 30484
diff changeset
   341
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   342
  Outer_Syntax.command "method_setup" "define proof method in ML" (Keyword.tag_ml Keyword.thy_decl)
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   343
    (Parse.position Parse.name -- Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Parse.text)
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   344
      >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
9197
16d88c5547bd added method_setup;
wenzelm
parents: 9129
diff changeset
   345
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   346
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   347
  Outer_Syntax.local_theory "declaration" "generic ML declaration" (Keyword.tag_ml Keyword.thy_decl)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   348
    (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry Isar_Cmd.declaration);
22088
4c53bb6e10e4 added 'declaration' command;
wenzelm
parents: 21956
diff changeset
   349
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   350
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   351
  Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   352
    (Parse.name --
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   353
      (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   354
      Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   355
    >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
22202
0544af1a5117 added simproc_setup;
wenzelm
parents: 22117
diff changeset
   356
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   357
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   358
(* translation functions *)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   359
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   360
val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
14642
2bfe5de2d1fa improved constdefs and translation functions;
wenzelm
parents: 14528
diff changeset
   361
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   362
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   363
  Outer_Syntax.command "parse_ast_translation" "install parse ast translation functions"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   364
    (Keyword.tag_ml Keyword.thy_decl)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   365
    (trfun >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   366
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   367
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   368
  Outer_Syntax.command "parse_translation" "install parse translation functions"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   369
    (Keyword.tag_ml Keyword.thy_decl)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   370
    (trfun >> (Toplevel.theory o Isar_Cmd.parse_translation));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   371
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   372
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   373
  Outer_Syntax.command "print_translation" "install print translation functions"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   374
    (Keyword.tag_ml Keyword.thy_decl)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   375
    (trfun >> (Toplevel.theory o Isar_Cmd.print_translation));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   376
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   377
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   378
  Outer_Syntax.command "typed_print_translation" "install typed print translation functions"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   379
    (Keyword.tag_ml Keyword.thy_decl)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   380
    (trfun >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   381
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   382
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   383
  Outer_Syntax.command "print_ast_translation" "install print ast translation functions"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   384
    (Keyword.tag_ml Keyword.thy_decl)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   385
    (trfun >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   386
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   387
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   388
(* oracles *)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   389
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   390
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   391
  Outer_Syntax.command "oracle" "declare oracle" (Keyword.tag_ml Keyword.thy_decl)
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   392
    (Parse.position Parse.name -- (Parse.$$$ "=" |-- Parse.ML_source) >>
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   393
      (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   394
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   395
21306
7ab6e95e6b0b turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents: 21269
diff changeset
   396
(* local theories *)
7ab6e95e6b0b turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents: 21269
diff changeset
   397
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   398
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   399
  Outer_Syntax.command "context" "enter local theory context" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   400
    (Parse.name --| Parse.begin >> (fn name =>
38350
480b2de9927c renamed Theory_Target to the more appropriate Named_Target
haftmann
parents: 38348
diff changeset
   401
      Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
21306
7ab6e95e6b0b turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents: 21269
diff changeset
   402
7ab6e95e6b0b turned 'context' into plain thy_decl, discontinued thy_switch;
wenzelm
parents: 21269
diff changeset
   403
12061
1b77d46d0fd1 added 'locale', 'print_locales', 'print_locale';
wenzelm
parents: 12044
diff changeset
   404
(* locales *)
1b77d46d0fd1 added 'locale', 'print_locales', 'print_locale';
wenzelm
parents: 12044
diff changeset
   405
12758
f6aceb9d4b8e print_locale: allow full body specification;
wenzelm
parents: 12712
diff changeset
   406
val locale_val =
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   407
  Parse_Spec.locale_expression false --
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   408
    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   409
  Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
12061
1b77d46d0fd1 added 'locale', 'print_locales', 'print_locale';
wenzelm
parents: 12044
diff changeset
   410
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   411
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   412
  Outer_Syntax.command "locale" "define named proof context" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   413
    (Parse.binding --
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   414
      Scan.optional (Parse.$$$ "=" |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
27681
8cedebf55539 dropped locale (open)
haftmann
parents: 27617
diff changeset
   415
      >> (fn ((name, (expr, elems)), begin) =>
21843
2015be1b6a03 locale: print context for begin;
wenzelm
parents: 21800
diff changeset
   416
          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
30344
10a67c5ddddb more uniform handling of binding in targets and derived elements;
wenzelm
parents: 30334
diff changeset
   417
            (Expression.add_locale_cmd name Binding.empty expr elems #> snd)));
28085
914183e229e9 Interpretation commands no longer accept interpretation attributes.
ballarin
parents: 28084
diff changeset
   418
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   419
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   420
  Outer_Syntax.command "sublocale"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   421
    "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   422
    (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   423
      Parse.!!! (Parse_Spec.locale_expression false)
28895
4e2914c2f8c5 Sublocale command.
ballarin
parents: 28820
diff changeset
   424
      >> (fn (loc, expr) =>
30727
519f8f0fcbf3 interpretation/interpret: prefixes within locale expression are mandatory by default;
wenzelm
parents: 30703
diff changeset
   425
          Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)));
28895
4e2914c2f8c5 Sublocale command.
ballarin
parents: 28820
diff changeset
   426
4e2914c2f8c5 Sublocale command.
ballarin
parents: 28820
diff changeset
   427
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   428
  Outer_Syntax.command "interpretation"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   429
    "prove interpretation of locale expression in theory" Keyword.thy_goal
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   430
    (Parse.!!! (Parse_Spec.locale_expression true) --
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   431
      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
30727
519f8f0fcbf3 interpretation/interpret: prefixes within locale expression are mandatory by default;
wenzelm
parents: 30703
diff changeset
   432
      >> (fn (expr, equations) => Toplevel.print o
519f8f0fcbf3 interpretation/interpret: prefixes within locale expression are mandatory by default;
wenzelm
parents: 30703
diff changeset
   433
          Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
29223
e09c53289830 Conversion of HOL-Main and ZF to new locales.
ballarin
parents: 29033
diff changeset
   434
e09c53289830 Conversion of HOL-Main and ZF to new locales.
ballarin
parents: 29033
diff changeset
   435
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   436
  Outer_Syntax.command "interpret"
29223
e09c53289830 Conversion of HOL-Main and ZF to new locales.
ballarin
parents: 29033
diff changeset
   437
    "prove interpretation of locale expression in proof context"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   438
    (Keyword.tag_proof Keyword.prf_goal)
38108
b4115423c049 Interpretation in proofs supports mixins.
ballarin
parents: 37987
diff changeset
   439
    (Parse.!!! (Parse_Spec.locale_expression true) --
b4115423c049 Interpretation in proofs supports mixins.
ballarin
parents: 37987
diff changeset
   440
      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
b4115423c049 Interpretation in proofs supports mixins.
ballarin
parents: 37987
diff changeset
   441
      >> (fn (expr, equations) => Toplevel.print o
b4115423c049 Interpretation in proofs supports mixins.
ballarin
parents: 37987
diff changeset
   442
          Toplevel.proof' (Expression.interpret_cmd expr equations)));
29223
e09c53289830 Conversion of HOL-Main and ZF to new locales.
ballarin
parents: 29033
diff changeset
   443
15703
727ef1b8b3ee *** empty log message ***
wenzelm
parents: 15624
diff changeset
   444
22299
a1293efe7ea5 moved commands of class package here
haftmann
parents: 22239
diff changeset
   445
(* classes *)
a1293efe7ea5 moved commands of class package here
haftmann
parents: 22239
diff changeset
   446
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   447
val class_val =
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   448
  Parse_Spec.class_expr --
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   449
    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   450
  Scan.repeat1 Parse_Spec.context_element >> pair [];
22299
a1293efe7ea5 moved commands of class package here
haftmann
parents: 22239
diff changeset
   451
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   452
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   453
  Outer_Syntax.command "class" "define type class" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   454
   (Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin
26516
1bf210ac0a90 removed obscure "attach" feature
haftmann
parents: 26490
diff changeset
   455
    >> (fn ((name, (supclasses, elems)), begin) =>
24938
a220317465b4 class: print result is for locale;
wenzelm
parents: 24932
diff changeset
   456
        (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
38379
67d71449e85b more convenient split of class modules: class and class_declaration
haftmann
parents: 38350
diff changeset
   457
          (Class_Declaration.class_cmd name supclasses elems #> snd)));
22299
a1293efe7ea5 moved commands of class package here
haftmann
parents: 22239
diff changeset
   458
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   459
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   460
  Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
38379
67d71449e85b more convenient split of class modules: class and class_declaration
haftmann
parents: 38350
diff changeset
   461
    (Parse.xname >> Class_Declaration.subclass_cmd);
24914
95cda5dd58d5 added proper subclass concept; improved class target
haftmann
parents: 24871
diff changeset
   462
95cda5dd58d5 added proper subclass concept; improved class target
haftmann
parents: 24871
diff changeset
   463
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   464
  Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   465
   (Parse.multi_arity --| Parse.begin
25462
dad0291cb76a rudimentary instantiation target
haftmann
parents: 25290
diff changeset
   466
     >> (fn arities => Toplevel.print o
38348
cf7b2121ad9d moved instantiation target formally to class_target.ML
haftmann
parents: 38342
diff changeset
   467
         Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
24589
d3fca349736c clarified class interfaces and internals
haftmann
parents: 24451
diff changeset
   468
25485
33840a854e63 tuned interfaces of class module
haftmann
parents: 25462
diff changeset
   469
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   470
  Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   471
  ((Parse.xname -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.xname)
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   472
        >> Class.classrel_cmd ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   473
    Parse.multi_arity >> Class.instance_arity_cmd)
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   474
    >> (Toplevel.print oo Toplevel.theory_to_proof) ||
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   475
    Scan.succeed
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   476
      (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
22299
a1293efe7ea5 moved commands of class package here
haftmann
parents: 22239
diff changeset
   477
a1293efe7ea5 moved commands of class package here
haftmann
parents: 22239
diff changeset
   478
25519
8570745cb40b overloading target
haftmann
parents: 25502
diff changeset
   479
(* arbitrary overloading *)
8570745cb40b overloading target
haftmann
parents: 25502
diff changeset
   480
8570745cb40b overloading target
haftmann
parents: 25502
diff changeset
   481
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   482
  Outer_Syntax.command "overloading" "overloaded definitions" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   483
   (Scan.repeat1 (Parse.name --| (Parse.$$$ "\\<equiv>" || Parse.$$$ "==") -- Parse.term --
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   484
      Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   485
      >> Parse.triple1) --| Parse.begin
25519
8570745cb40b overloading target
haftmann
parents: 25502
diff changeset
   486
   >> (fn operations => Toplevel.print o
38342
09d4a04d5c2e moved overloading target formally to overloading.ML
haftmann
parents: 38108
diff changeset
   487
         Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
25519
8570745cb40b overloading target
haftmann
parents: 25502
diff changeset
   488
8570745cb40b overloading target
haftmann
parents: 25502
diff changeset
   489
22866
wenzelm
parents: 22796
diff changeset
   490
(* code generation *)
wenzelm
parents: 22796
diff changeset
   491
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   492
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   493
  Outer_Syntax.command "code_datatype" "define set of code datatype constructors" Keyword.thy_decl
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   494
    (Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
22866
wenzelm
parents: 22796
diff changeset
   495
wenzelm
parents: 22796
diff changeset
   496
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   497
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   498
(** proof commands **)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   499
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   500
(* statements *)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   501
36317
506d732cb522 explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents: 36178
diff changeset
   502
fun gen_theorem schematic kind =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   503
  Outer_Syntax.local_theory_to_proof'
36317
506d732cb522 explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents: 36178
diff changeset
   504
    (if schematic then "schematic_" ^ kind else kind)
506d732cb522 explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents: 36178
diff changeset
   505
    ("state " ^ (if schematic then "schematic " ^ kind else kind))
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   506
    (if schematic then Keyword.thy_schematic_goal else Keyword.thy_goal)
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   507
    (Scan.optional (Parse_Spec.opt_thm_name ":" --|
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   508
      Scan.ahead (Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   509
      Parse_Spec.general_statement >> (fn (a, (elems, concl)) =>
36317
506d732cb522 explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents: 36178
diff changeset
   510
        ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
506d732cb522 explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents: 36178
diff changeset
   511
          kind NONE (K I) a elems concl)));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   512
36317
506d732cb522 explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents: 36178
diff changeset
   513
val _ = gen_theorem false Thm.theoremK;
506d732cb522 explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents: 36178
diff changeset
   514
val _ = gen_theorem false Thm.lemmaK;
506d732cb522 explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents: 36178
diff changeset
   515
val _ = gen_theorem false Thm.corollaryK;
506d732cb522 explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents: 36178
diff changeset
   516
val _ = gen_theorem true Thm.theoremK;
506d732cb522 explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents: 36178
diff changeset
   517
val _ = gen_theorem true Thm.lemmaK;
506d732cb522 explicit 'schematic_theorem' etc. for schematic theorem statements;
wenzelm
parents: 36178
diff changeset
   518
val _ = gen_theorem true Thm.corollaryK;
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   519
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   520
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   521
  Outer_Syntax.local_theory_to_proof "example_proof"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   522
    "example proof body, without any result" Keyword.thy_schematic_goal
36356
5ab0f8859f9f command 'example_proof' opens an empty proof body;
wenzelm
parents: 36323
diff changeset
   523
    (Scan.succeed
5ab0f8859f9f command 'example_proof' opens an empty proof body;
wenzelm
parents: 36323
diff changeset
   524
      (Specification.schematic_theorem_cmd "" NONE (K I)
5ab0f8859f9f command 'example_proof' opens an empty proof body;
wenzelm
parents: 36323
diff changeset
   525
        Attrib.empty_binding [] (Element.Shows []) false #> Proof.enter_forward));
5ab0f8859f9f command 'example_proof' opens an empty proof body;
wenzelm
parents: 36323
diff changeset
   526
5ab0f8859f9f command 'example_proof' opens an empty proof body;
wenzelm
parents: 36323
diff changeset
   527
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   528
  Outer_Syntax.command "have" "state local goal"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   529
    (Keyword.tag_proof Keyword.prf_goal)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   530
    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
17353
cd440b6812b1 cleanup parsers and interfaces;
wenzelm
parents: 17264
diff changeset
   531
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   532
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   533
  Outer_Syntax.command "hence" "abbreviates \"then have\""
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   534
    (Keyword.tag_proof Keyword.prf_goal)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   535
    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
17353
cd440b6812b1 cleanup parsers and interfaces;
wenzelm
parents: 17264
diff changeset
   536
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   537
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   538
  Outer_Syntax.command "show" "state local goal, solving current obligation"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   539
    (Keyword.tag_proof Keyword.prf_asm_goal)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   540
    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   541
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   542
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   543
  Outer_Syntax.command "thus" "abbreviates \"then show\""
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   544
    (Keyword.tag_proof Keyword.prf_asm_goal)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   545
    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
6501
392333eb31cb added thus, hence;
wenzelm
parents: 6404
diff changeset
   546
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   547
5914
2c069b0a98ee added 'theorems', 'lemmas', 'note';
wenzelm
parents: 5896
diff changeset
   548
(* facts *)
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   549
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   550
val facts = Parse.and_list1 Parse_Spec.xthms1;
9197
16d88c5547bd added method_setup;
wenzelm
parents: 9129
diff changeset
   551
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   552
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   553
  Outer_Syntax.command "then" "forward chaining"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   554
    (Keyword.tag_proof Keyword.prf_chain)
17900
5f44c71c4ca4 use simplified Toplevel.proof etc.;
wenzelm
parents: 17854
diff changeset
   555
    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   556
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   557
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   558
  Outer_Syntax.command "from" "forward chaining from given facts"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   559
    (Keyword.tag_proof Keyword.prf_chain)
36323
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 36317
diff changeset
   560
    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
5914
2c069b0a98ee added 'theorems', 'lemmas', 'note';
wenzelm
parents: 5896
diff changeset
   561
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   562
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   563
  Outer_Syntax.command "with" "forward chaining from given and current facts"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   564
    (Keyword.tag_proof Keyword.prf_chain)
36323
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 36317
diff changeset
   565
    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
6878
1e97e7fbcca5 'with' as == 'from' as facts;
wenzelm
parents: 6869
diff changeset
   566
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   567
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   568
  Outer_Syntax.command "note" "define facts"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   569
    (Keyword.tag_proof Keyword.prf_decl)
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   570
    (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   571
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   572
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   573
  Outer_Syntax.command "using" "augment goal facts"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   574
    (Keyword.tag_proof Keyword.prf_decl)
36323
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 36317
diff changeset
   575
    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
18544
cbad888756b2 added 'using' command;
wenzelm
parents: 18308
diff changeset
   576
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   577
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   578
  Outer_Syntax.command "unfolding" "unfold definitions in goal and facts"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   579
    (Keyword.tag_proof Keyword.prf_decl)
36323
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 36317
diff changeset
   580
    (facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
12926
cd0dd6e0bf5c 'using' command;
wenzelm
parents: 12876
diff changeset
   581
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   582
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   583
(* proof context *)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   584
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   585
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   586
  Outer_Syntax.command "fix" "fix local variables (Skolem constants)"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   587
    (Keyword.tag_proof Keyword.prf_asm)
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   588
    (Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
11890
28e42a90bea8 improved source arrangement of obtain;
wenzelm
parents: 11793
diff changeset
   589
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   590
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   591
  Outer_Syntax.command "assume" "assume propositions"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   592
    (Keyword.tag_proof Keyword.prf_asm)
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   593
    (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   594
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   595
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   596
  Outer_Syntax.command "presume" "assume propositions, to be established later"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   597
    (Keyword.tag_proof Keyword.prf_asm)
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   598
    (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
6850
da8a4660fb0c added presume command;
wenzelm
parents: 6773
diff changeset
   599
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   600
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   601
  Outer_Syntax.command "def" "local definition"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   602
    (Keyword.tag_proof Keyword.prf_asm)
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   603
    (Parse.and_list1
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   604
      (Parse_Spec.opt_thm_name ":" --
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   605
        ((Parse.binding -- Parse.opt_mixfix) --
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   606
          ((Parse.$$$ "\\<equiv>" || Parse.$$$ "==") |-- Parse.!!! Parse.termp)))
36323
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 36317
diff changeset
   607
    >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
6953
b3f6c39aaa2e added 'def';
wenzelm
parents: 6936
diff changeset
   608
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   609
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   610
  Outer_Syntax.command "obtain" "generalized existence"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   611
    (Keyword.tag_proof Keyword.prf_asm_goal)
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   612
    (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
36323
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 36317
diff changeset
   613
      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   614
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   615
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   616
  Outer_Syntax.command "guess" "wild guessing (unstructured)"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   617
    (Keyword.tag_proof Keyword.prf_asm_goal)
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   618
    (Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
17854
44b6dde80bf4 added 'guess';
wenzelm
parents: 17512
diff changeset
   619
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   620
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   621
  Outer_Syntax.command "let" "bind text variables"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   622
    (Keyword.tag_proof Keyword.prf_decl)
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   623
    (Parse.and_list1 (Parse.and_list1 Parse.term -- (Parse.$$$ "=" |-- Parse.term))
36323
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 36317
diff changeset
   624
      >> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   625
36505
79c1d2bbe5a9 ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents: 36452
diff changeset
   626
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   627
  Outer_Syntax.command "write" "add concrete syntax for constants / fixed variables"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   628
    (Keyword.tag_proof Keyword.prf_decl)
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   629
    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
36505
79c1d2bbe5a9 ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents: 36452
diff changeset
   630
    >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
79c1d2bbe5a9 ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents: 36452
diff changeset
   631
11793
5f0ab6f5c280 support impromptu terminology of cases parameters;
wenzelm
parents: 11742
diff changeset
   632
val case_spec =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   633
  (Parse.$$$ "(" |--
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   634
    Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.name) --| Parse.$$$ ")") ||
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   635
    Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1;
11793
5f0ab6f5c280 support impromptu terminology of cases parameters;
wenzelm
parents: 11742
diff changeset
   636
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   637
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   638
  Outer_Syntax.command "case" "invoke local context"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   639
    (Keyword.tag_proof Keyword.prf_asm)
36323
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 36317
diff changeset
   640
    (case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
8370
6b45749d37d6 added 'case' command;
wenzelm
parents: 8349
diff changeset
   641
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   642
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   643
(* proof structure *)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   644
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   645
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   646
  Outer_Syntax.command "{" "begin explicit proof block"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   647
    (Keyword.tag_proof Keyword.prf_open)
17900
5f44c71c4ca4 use simplified Toplevel.proof etc.;
wenzelm
parents: 17854
diff changeset
   648
    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   649
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   650
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   651
  Outer_Syntax.command "}" "end explicit proof block"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   652
    (Keyword.tag_proof Keyword.prf_close)
20305
16c8f44b1852 simplified Proof.end_block;
wenzelm
parents: 19844
diff changeset
   653
    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
6687
134df1440f6e renamed 'begin' / 'end' to '{{' / '}}';
wenzelm
parents: 6551
diff changeset
   654
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   655
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   656
  Outer_Syntax.command "next" "enter next proof block"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   657
    (Keyword.tag_proof Keyword.prf_block)
17900
5f44c71c4ca4 use simplified Toplevel.proof etc.;
wenzelm
parents: 17854
diff changeset
   658
    (Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   659
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   660
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   661
(* end proof *)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   662
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   663
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   664
  Outer_Syntax.command "qed" "conclude (sub-)proof"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   665
    (Keyword.tag_proof Keyword.qed_block)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   666
    (Scan.option Method.parse >> Isar_Cmd.qed);
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   667
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   668
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   669
  Outer_Syntax.command "by" "terminal backward proof"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   670
    (Keyword.tag_proof Keyword.qed)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   671
    (Method.parse -- Scan.option Method.parse >> Isar_Cmd.terminal_proof);
6404
2daaf2943c79 common qed and end of proofs;
wenzelm
parents: 6370
diff changeset
   672
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   673
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   674
  Outer_Syntax.command ".." "default proof"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   675
    (Keyword.tag_proof Keyword.qed)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   676
    (Scan.succeed Isar_Cmd.default_proof);
8966
916966f68907 added "done" proof;
wenzelm
parents: 8896
diff changeset
   677
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   678
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   679
  Outer_Syntax.command "." "immediate proof"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   680
    (Keyword.tag_proof Keyword.qed)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   681
    (Scan.succeed Isar_Cmd.immediate_proof);
6404
2daaf2943c79 common qed and end of proofs;
wenzelm
parents: 6370
diff changeset
   682
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   683
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   684
  Outer_Syntax.command "done" "done proof"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   685
    (Keyword.tag_proof Keyword.qed)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   686
    (Scan.succeed Isar_Cmd.done_proof);
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   687
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   688
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   689
  Outer_Syntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   690
    (Keyword.tag_proof Keyword.qed)
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   691
    (Scan.succeed Isar_Cmd.skip_proof);
6888
d0c68ebdabc5 skip_proof feature 'sorry' (for quick_and_dirty mode only);
wenzelm
parents: 6886
diff changeset
   692
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   693
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   694
  Outer_Syntax.command "oops" "forget proof"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   695
    (Keyword.tag_proof Keyword.qed_global)
18561
b0e134637479 Toplevel.forget_proof;
wenzelm
parents: 18544
diff changeset
   696
    (Scan.succeed Toplevel.forget_proof);
8210
ca3997312f47 added forget_proof;
wenzelm
parents: 8165
diff changeset
   697
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   698
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   699
(* proof steps *)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   700
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   701
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   702
  Outer_Syntax.command "defer" "shuffle internal proof state"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   703
    (Keyword.tag_proof Keyword.prf_script)
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   704
    (Scan.option Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
8165
651b006d7eb8 added defer, prefer;
wenzelm
parents: 8097
diff changeset
   705
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   706
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   707
  Outer_Syntax.command "prefer" "shuffle internal proof state"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   708
    (Keyword.tag_proof Keyword.prf_script)
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   709
    (Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
8165
651b006d7eb8 added defer, prefer;
wenzelm
parents: 8097
diff changeset
   710
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   711
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   712
  Outer_Syntax.command "apply" "initial refinement step (unstructured)"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   713
    (Keyword.tag_proof Keyword.prf_script)
22117
505e040bdcdb renamed IsarOutput to ThyOutput;
wenzelm
parents: 22088
diff changeset
   714
    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   715
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   716
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   717
  Outer_Syntax.command "apply_end" "terminal refinement (unstructured)"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   718
    (Keyword.tag_proof Keyword.prf_script)
22117
505e040bdcdb renamed IsarOutput to ThyOutput;
wenzelm
parents: 22088
diff changeset
   719
    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   720
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   721
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   722
  Outer_Syntax.command "proof" "backward proof"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   723
    (Keyword.tag_proof Keyword.prf_block)
22117
505e040bdcdb renamed IsarOutput to ThyOutput;
wenzelm
parents: 22088
diff changeset
   724
    (Scan.option Method.parse >> (fn m => Toplevel.print o
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33287
diff changeset
   725
      Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o
27563
38f26d4079be removed obsolete 'redo' command;
wenzelm
parents: 27534
diff changeset
   726
      Toplevel.skip_proof (fn i => i + 1)));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   727
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   728
6773
83c09a9684cf added 'also', 'finally' commands;
wenzelm
parents: 6757
diff changeset
   729
(* calculational proof commands *)
83c09a9684cf added 'also', 'finally' commands;
wenzelm
parents: 6757
diff changeset
   730
6878
1e97e7fbcca5 'with' as == 'from' as facts;
wenzelm
parents: 6869
diff changeset
   731
val calc_args =
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   732
  Scan.option (Parse.$$$ "(" |-- Parse.!!! ((Parse_Spec.xthms1 --| Parse.$$$ ")")));
6878
1e97e7fbcca5 'with' as == 'from' as facts;
wenzelm
parents: 6869
diff changeset
   733
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   734
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   735
  Outer_Syntax.command "also" "combine calculation and current facts"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   736
    (Keyword.tag_proof Keyword.prf_decl)
36323
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 36317
diff changeset
   737
    (calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
6773
83c09a9684cf added 'also', 'finally' commands;
wenzelm
parents: 6757
diff changeset
   738
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   739
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   740
  Outer_Syntax.command "finally" "combine calculation and current facts, exhibit result"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   741
    (Keyword.tag_proof Keyword.prf_chain)
36323
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 36317
diff changeset
   742
    (calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
6773
83c09a9684cf added 'also', 'finally' commands;
wenzelm
parents: 6757
diff changeset
   743
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   744
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   745
  Outer_Syntax.command "moreover" "augment calculation by current facts"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   746
    (Keyword.tag_proof Keyword.prf_decl)
17900
5f44c71c4ca4 use simplified Toplevel.proof etc.;
wenzelm
parents: 17854
diff changeset
   747
    (Scan.succeed (Toplevel.proof' Calculation.moreover));
8562
ce0e2b8e8844 added 'moreover' command;
wenzelm
parents: 8521
diff changeset
   748
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   749
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   750
  Outer_Syntax.command "ultimately" "augment calculation by current facts, exhibit result"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   751
    (Keyword.tag_proof Keyword.prf_chain)
17900
5f44c71c4ca4 use simplified Toplevel.proof etc.;
wenzelm
parents: 17854
diff changeset
   752
    (Scan.succeed (Toplevel.proof' Calculation.ultimately));
8588
b7c3f264f8ac added 'ultimately';
wenzelm
parents: 8562
diff changeset
   753
6773
83c09a9684cf added 'also', 'finally' commands;
wenzelm
parents: 6757
diff changeset
   754
6742
6b5cb872d997 improved undo / kill operations;
wenzelm
parents: 6735
diff changeset
   755
(* proof navigation *)
5944
dcc446da8e19 added undos, redos;
wenzelm
parents: 5937
diff changeset
   756
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   757
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   758
  Outer_Syntax.command "back" "backtracking of proof command"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   759
    (Keyword.tag_proof Keyword.prf_script)
33390
5b499f36dd25 modernized structure Proof_Node;
wenzelm
parents: 33287
diff changeset
   760
    (Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I));
6742
6b5cb872d997 improved undo / kill operations;
wenzelm
parents: 6735
diff changeset
   761
22744
5cbe966d67a2 Isar definitions are now added explicitly to code theorem table
haftmann
parents: 22573
diff changeset
   762
27614
f38c25d106a7 renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
wenzelm
parents: 27575
diff changeset
   763
(* nested commands *)
25578
11ee8b183477 added nested 'Isabelle.command';
wenzelm
parents: 25536
diff changeset
   764
29309
aa6d11fbe3b6 added props_text (from outer_parse.ML);
wenzelm
parents: 29225
diff changeset
   765
val props_text =
36951
985c197f2fe9 renamed structure ValueParse to Parse_Value;
wenzelm
parents: 36950
diff changeset
   766
  Scan.optional Parse_Value.properties [] -- Parse.position Parse.string
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   767
  >> (fn (props, (str, pos)) =>
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   768
      (Position.of_properties (Position.default_properties pos props), str));
29309
aa6d11fbe3b6 added props_text (from outer_parse.ML);
wenzelm
parents: 29225
diff changeset
   769
25578
11ee8b183477 added nested 'Isabelle.command';
wenzelm
parents: 25536
diff changeset
   770
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   771
  Outer_Syntax.improper_command "Isabelle.command" "nested Isabelle command" Keyword.control
29309
aa6d11fbe3b6 added props_text (from outer_parse.ML);
wenzelm
parents: 29225
diff changeset
   772
    (props_text :|-- (fn (pos, str) =>
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   773
      (case Outer_Syntax.parse pos str of
27838
0340fd7cccc3 Isabelle.command: inline former OuterSyntax.prepare_command;
wenzelm
parents: 27831
diff changeset
   774
        [tr] => Scan.succeed (K tr)
0340fd7cccc3 Isabelle.command: inline former OuterSyntax.prepare_command;
wenzelm
parents: 27831
diff changeset
   775
      | _ => Scan.fail_with (K "exactly one command expected"))
0340fd7cccc3 Isabelle.command: inline former OuterSyntax.prepare_command;
wenzelm
parents: 27831
diff changeset
   776
      handle ERROR msg => Scan.fail_with (K msg)));
25578
11ee8b183477 added nested 'Isabelle.command';
wenzelm
parents: 25536
diff changeset
   777
11ee8b183477 added nested 'Isabelle.command';
wenzelm
parents: 25536
diff changeset
   778
22744
5cbe966d67a2 Isar definitions are now added explicitly to code theorem table
haftmann
parents: 22573
diff changeset
   779
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   780
(** diagnostic commands (for interactive mode only) **)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   781
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   782
val opt_modes =
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   783
  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Scan.repeat1 Parse.xname --| Parse.$$$ ")")) [];
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   784
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   785
val opt_bang = Scan.optional (Parse.$$$ "!" >> K true) false;
8464
0f78101b249a 'pr': modes, optional limit;
wenzelm
parents: 8454
diff changeset
   786
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   787
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   788
  Outer_Syntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
38870
wenzelm
parents: 38708
diff changeset
   789
    Keyword.diag (Parse.nat >>
wenzelm
parents: 38708
diff changeset
   790
      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Pretty.margin_default := n)));
7124
78c01842d3b5 added pretty_setmargin;
wenzelm
parents: 7102
diff changeset
   791
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   792
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   793
  Outer_Syntax.improper_command "help" "print outer syntax commands" Keyword.diag
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   794
    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
21714
d64cb19c79e2 added 'help' command (same of 'print_commands');
wenzelm
parents: 21705
diff changeset
   795
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   796
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   797
  Outer_Syntax.improper_command "print_commands" "print outer syntax commands" Keyword.diag
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   798
    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   799
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   800
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   801
  Outer_Syntax.improper_command "print_configs" "print configuration options" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   802
    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_configs));
23989
d7df8545f9f6 added command 'print_options';
wenzelm
parents: 23865
diff changeset
   803
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   804
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   805
  Outer_Syntax.improper_command "print_context" "print theory context name" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   806
    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_context));
7308
e01aab03a2a1 print_context;
wenzelm
parents: 7269
diff changeset
   807
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   808
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   809
  Outer_Syntax.improper_command "print_theory" "print logical theory contents (verbose!)"
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   810
    Keyword.diag (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theory));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   811
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   812
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   813
  Outer_Syntax.improper_command "print_syntax" "print inner syntax of context (verbose!)"
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   814
    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_syntax));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   815
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   816
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   817
  Outer_Syntax.improper_command "print_abbrevs" "print constant abbreviation of context"
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   818
    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_abbrevs));
21726
092b967da9b7 added 'print_abbrevs';
wenzelm
parents: 21714
diff changeset
   819
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   820
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   821
  Outer_Syntax.improper_command "print_theorems"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   822
      "print theorems of local theory or proof context" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   823
    (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theorems));
5881
2bded7137593 add print_theorems;
wenzelm
parents: 5832
diff changeset
   824
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   825
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   826
  Outer_Syntax.improper_command "print_locales" "print locales of this theory" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   827
    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_locales));
12061
1b77d46d0fd1 added 'locale', 'print_locales', 'print_locale';
wenzelm
parents: 12044
diff changeset
   828
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   829
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   830
  Outer_Syntax.improper_command "print_classes" "print classes of this theory" Keyword.diag
22744
5cbe966d67a2 Isar definitions are now added explicitly to code theorem table
haftmann
parents: 22573
diff changeset
   831
    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory
24219
e558fe311376 new structure for code generator modules
haftmann
parents: 24174
diff changeset
   832
      o Toplevel.keep (Class.print_classes o Toplevel.theory_of)));
22744
5cbe966d67a2 Isar definitions are now added explicitly to code theorem table
haftmann
parents: 22573
diff changeset
   833
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   834
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   835
  Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   836
    (opt_bang -- Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
12061
1b77d46d0fd1 added 'locale', 'print_locales', 'print_locale';
wenzelm
parents: 12044
diff changeset
   837
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   838
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   839
  Outer_Syntax.improper_command "print_interps"
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   840
    "print interpretations of locale for this theory" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   841
    (Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
32804
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 31869
diff changeset
   842
ca430e6aee1c Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
ballarin
parents: 31869
diff changeset
   843
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   844
  Outer_Syntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   845
    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   846
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   847
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   848
  Outer_Syntax.improper_command "print_simpset" "print context of Simplifier" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   849
    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_simpset));
16027
77c1171090d9 added 'print_simpset';
wenzelm
parents: 15979
diff changeset
   850
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   851
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   852
  Outer_Syntax.improper_command "print_rules" "print intro/elim rules" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   853
    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_rules));
12383
af14fd56b189 added 'print_rules' command;
wenzelm
parents: 12288
diff changeset
   854
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   855
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   856
  Outer_Syntax.improper_command "print_trans_rules" "print transitivity rules" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   857
    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_trans_rules));
9221
e1fd1003d5f9 removed "help";
wenzelm
parents: 9197
diff changeset
   858
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   859
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   860
  Outer_Syntax.improper_command "print_methods" "print methods of this theory" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   861
    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_methods));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   862
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   863
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   864
  Outer_Syntax.improper_command "print_antiquotations" "print antiquotations (global)" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   865
    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_antiquotations));
9221
e1fd1003d5f9 removed "help";
wenzelm
parents: 9197
diff changeset
   866
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   867
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   868
  Outer_Syntax.improper_command "thy_deps" "visualize theory dependencies"
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   869
    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
22485
3a7d623485fa added theory dependency graph
haftmann
parents: 22417
diff changeset
   870
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   871
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   872
  Outer_Syntax.improper_command "class_deps" "visualize class dependencies"
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   873
    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
20574
a10885a269cb added class_deps;
wenzelm
parents: 20365
diff changeset
   874
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   875
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   876
  Outer_Syntax.improper_command "thm_deps" "visualize theorem dependencies"
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   877
    Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));
9454
ea80449107cc added thm_deps;
wenzelm
parents: 9323
diff changeset
   878
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   879
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   880
  Outer_Syntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   881
    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_binds));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   882
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   883
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   884
  Outer_Syntax.improper_command "print_facts" "print facts of proof context" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   885
    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_facts));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   886
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   887
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   888
  Outer_Syntax.improper_command "print_cases" "print cases of proof context" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   889
    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_cases));
8370
6b45749d37d6 added 'case' command;
wenzelm
parents: 8349
diff changeset
   890
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   891
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   892
  Outer_Syntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   893
    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_stmts));
19269
620616bc7632 added 'print_statement' command;
wenzelm
parents: 19260
diff changeset
   894
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   895
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   896
  Outer_Syntax.improper_command "thm" "print theorems" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   897
    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_thms));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   898
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   899
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   900
  Outer_Syntax.improper_command "prf" "print proof terms of theorems" Keyword.diag
36952
338c3f8229e4 renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents: 36951
diff changeset
   901
    (opt_modes -- Scan.option Parse_Spec.xthms1
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   902
      >> (Toplevel.no_timing oo Isar_Cmd.print_prfs false));
11524
197f2e14a714 Added functions for printing primitive proof terms.
berghofe
parents: 11101
diff changeset
   903
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   904
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   905
  Outer_Syntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   906
    (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_prfs true));
11524
197f2e14a714 Added functions for printing primitive proof terms.
berghofe
parents: 11101
diff changeset
   907
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   908
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   909
  Outer_Syntax.improper_command "prop" "read and print proposition" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   910
    (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_prop));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   911
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   912
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   913
  Outer_Syntax.improper_command "term" "read and print term" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   914
    (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_term));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   915
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   916
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   917
  Outer_Syntax.improper_command "typ" "read and print type" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   918
    (opt_modes -- Parse.typ >> (Toplevel.no_timing oo Isar_Cmd.print_type));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   919
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   920
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   921
  Outer_Syntax.improper_command "print_codesetup" "print code generator setup" Keyword.diag
22744
5cbe966d67a2 Isar definitions are now added explicitly to code theorem table
haftmann
parents: 22573
diff changeset
   922
    (Scan.succeed
5cbe966d67a2 Isar definitions are now added explicitly to code theorem table
haftmann
parents: 22573
diff changeset
   923
      (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
24219
e558fe311376 new structure for code generator modules
haftmann
parents: 24174
diff changeset
   924
        (Code.print_codesetup o Toplevel.theory_of)));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   925
26184
64ee6a2ca6d6 Added unused_thms command.
berghofe
parents: 26048
diff changeset
   926
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   927
  Outer_Syntax.improper_command "unused_thms" "find unused theorems" Keyword.diag
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   928
    (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   929
       Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   930
         (Toplevel.no_timing oo Isar_Cmd.unused_thms));
26184
64ee6a2ca6d6 Added unused_thms command.
berghofe
parents: 26048
diff changeset
   931
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   932
30142
8d6145694bb5 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;
wenzelm
parents: 29882
diff changeset
   933
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   934
(** system commands (for interactive mode only) **)
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   935
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   936
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   937
  Outer_Syntax.improper_command "cd" "change current working directory" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   938
    (Parse.path >> (Toplevel.no_timing oo Isar_Cmd.cd));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   939
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   940
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   941
  Outer_Syntax.improper_command "pwd" "print current working directory" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   942
    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.pwd));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   943
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   944
val _ =
37987
aac4eb1fa1d8 explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents;
wenzelm
parents: 37981
diff changeset
   945
  Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.control
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   946
    (Parse.name >> (fn name =>
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   947
      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   948
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   949
val _ =
37987
aac4eb1fa1d8 explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents;
wenzelm
parents: 37981
diff changeset
   950
  Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.control
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   951
    (Parse.name >> (fn name =>
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   952
      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
7102
ead5c234b28c removed update_context;
wenzelm
parents: 7023
diff changeset
   953
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   954
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   955
  Outer_Syntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
37987
aac4eb1fa1d8 explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents;
wenzelm
parents: 37981
diff changeset
   956
    Keyword.control (Parse.name >> (fn name =>
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   957
      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
7931
fa6fec415492 added kill_thy;
wenzelm
parents: 7908
diff changeset
   958
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   959
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   960
  Outer_Syntax.improper_command "display_drafts" "display raw source files with symbols"
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   961
    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));
14934
bf9f525d4821 added display_drafts and print_drafts commands;
wenzelm
parents: 14900
diff changeset
   962
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   963
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   964
  Outer_Syntax.improper_command "print_drafts" "print raw source files with symbols"
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   965
    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
14934
bf9f525d4821 added display_drafts and print_drafts commands;
wenzelm
parents: 14900
diff changeset
   966
9731
3eb72671e5db pr: added prems limit;
wenzelm
parents: 9589
diff changeset
   967
val opt_limits =
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   968
  Scan.option Parse.nat -- Scan.option (Parse.$$$ "," |-- Parse.!!! Parse.nat);
9731
3eb72671e5db pr: added prems limit;
wenzelm
parents: 9589
diff changeset
   969
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   970
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   971
  Outer_Syntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   972
    (opt_modes -- opt_limits >> (Toplevel.no_timing oo Isar_Cmd.pr));
7199
7fede88e5c73 pr / no_pr: maintain Toplevel.quiet;
wenzelm
parents: 7172
diff changeset
   973
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   974
val _ =
37987
aac4eb1fa1d8 explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents;
wenzelm
parents: 37981
diff changeset
   975
  Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.control
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   976
    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.disable_pr));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   977
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   978
val _ =
37987
aac4eb1fa1d8 explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents;
wenzelm
parents: 37981
diff changeset
   979
  Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.control
37216
3165bc303f66 modernized some structure names, keeping a few legacy aliases;
wenzelm
parents: 37198
diff changeset
   980
    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.enable_pr));
7222
e4244b2e70ef disable_pr, enable_pr;
wenzelm
parents: 7199
diff changeset
   981
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   982
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   983
  Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.diag
36950
75b8f26f2f07 refer directly to structure Keyword and Parse;
wenzelm
parents: 36865
diff changeset
   984
    (Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   985
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   986
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   987
  Outer_Syntax.improper_command "quit" "quit Isabelle" Keyword.control
37977
3ceccd415145 simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents: 37949
diff changeset
   988
    (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative quit)));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   989
24868
2990c327d8c6 simplified interfaces for outer syntax;
wenzelm
parents: 24830
diff changeset
   990
val _ =
36953
2af1ad9aa1a3 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
wenzelm
parents: 36952
diff changeset
   991
  Outer_Syntax.improper_command "exit" "exit Isar loop" Keyword.control
37977
3ceccd415145 simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents: 37949
diff changeset
   992
    (Scan.succeed
3ceccd415145 simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents: 37949
diff changeset
   993
      (Toplevel.no_timing o Toplevel.keep (fn state =>
3ceccd415145 simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents: 37949
diff changeset
   994
        (Context.set_thread_data (try Toplevel.generic_theory_of state);
38888
8248cda328de moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents: 38870
diff changeset
   995
          raise Runtime.TERMINATE))));
5832
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   996
112a67aa9c2c Pure outer syntax.
wenzelm
parents:
diff changeset
   997
end;
27614
f38c25d106a7 renamed IsarCmd.nested_command to OuterSyntax.prepare_command;
wenzelm
parents: 27575
diff changeset
   998