src/Pure/Isar/isar_syn.ML
changeset 6723 f342449d73ca
parent 6694 335833a8b10a
child 6727 c8dba1da73cc
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon May 24 21:56:14 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon May 24 21:57:13 1999 +0200
     1.3 @@ -14,30 +14,30 @@
     1.4  structure IsarSyn: ISAR_SYN =
     1.5  struct
     1.6  
     1.7 -open OuterParse;
     1.8 +structure P = OuterParse and K = OuterSyntax.Keyword;
     1.9  
    1.10  
    1.11  (** init and exit **)
    1.12  
    1.13  val theoryP =
    1.14 -  OuterSyntax.command "theory" "begin theory"
    1.15 +  OuterSyntax.command "theory" "begin theory" K.thy_begin
    1.16      (OuterSyntax.theory_header >> (Toplevel.print oo IsarThy.theory));
    1.17  
    1.18  val end_excursionP =
    1.19 -  OuterSyntax.command "end" "end current excursion"
    1.20 +  OuterSyntax.command "end" "end current excursion" K.thy_end
    1.21      (Scan.succeed (Toplevel.print o Toplevel.exit));
    1.22  
    1.23  val kill_excursionP =
    1.24 -  OuterSyntax.command "kill" "kill current excursion"
    1.25 +  OuterSyntax.command "kill" "kill current excursion" K.control
    1.26      (Scan.succeed (Toplevel.print o Toplevel.kill));
    1.27  
    1.28  val contextP =
    1.29 -  OuterSyntax.improper_command "context" "switch theory context"
    1.30 -    (name >> (Toplevel.print oo IsarThy.context));
    1.31 +  OuterSyntax.improper_command "context" "switch theory context" K.thy_begin
    1.32 +    (P.name >> (Toplevel.print oo IsarThy.context));
    1.33  
    1.34  val update_contextP =
    1.35 -  OuterSyntax.improper_command "update_context" "switch theory context, forcing update"
    1.36 -    (name >> (Toplevel.print oo IsarThy.update_context));
    1.37 +  OuterSyntax.improper_command "update_context" "switch theory context, forcing update" K.thy_begin
    1.38 +    (P.name >> (Toplevel.print oo IsarThy.update_context));
    1.39  
    1.40  
    1.41  
    1.42 @@ -45,190 +45,190 @@
    1.43  
    1.44  (* formal comments *)
    1.45  
    1.46 -val textP = OuterSyntax.command "text" "formal comments"
    1.47 -  (comment >> (Toplevel.theory o IsarThy.add_text));
    1.48 +val textP = OuterSyntax.command "text" "formal comments" K.thy_decl
    1.49 +  (P.comment >> (Toplevel.theory o IsarThy.add_text));
    1.50  
    1.51 -val titleP = OuterSyntax.command "title" "document title"
    1.52 -  ((comment -- Scan.optional comment Comment.empty -- Scan.optional comment Comment.empty)
    1.53 +val titleP = OuterSyntax.command "title" "document title" K.thy_heading
    1.54 +  ((P.comment -- Scan.optional P.comment Comment.empty -- Scan.optional P.comment Comment.empty)
    1.55      >> (fn ((x, y), z) => Toplevel.theory (IsarThy.add_title x y z)));
    1.56  
    1.57 -val chapterP = OuterSyntax.command "chapter" "chapter heading"
    1.58 -  (comment >> (Toplevel.theory o IsarThy.add_chapter));
    1.59 +val chapterP = OuterSyntax.command "chapter" "chapter heading" K.thy_heading
    1.60 +  (P.comment >> (Toplevel.theory o IsarThy.add_chapter));
    1.61  
    1.62 -val sectionP = OuterSyntax.command "section" "section heading"
    1.63 -  (comment >> (Toplevel.theory o IsarThy.add_section));
    1.64 +val sectionP = OuterSyntax.command "section" "section heading" K.thy_heading
    1.65 +  (P.comment >> (Toplevel.theory o IsarThy.add_section));
    1.66  
    1.67 -val subsectionP = OuterSyntax.command "subsection" "subsection heading"
    1.68 -  (comment >> (Toplevel.theory o IsarThy.add_subsection));
    1.69 +val subsectionP = OuterSyntax.command "subsection" "subsection heading" K.thy_heading
    1.70 +  (P.comment >> (Toplevel.theory o IsarThy.add_subsection));
    1.71  
    1.72 -val subsubsectionP = OuterSyntax.command "subsubsection" "subsubsection heading"
    1.73 -  (comment >> (Toplevel.theory o IsarThy.add_subsubsection));
    1.74 +val subsubsectionP = OuterSyntax.command "subsubsection" "subsubsection heading" K.thy_heading
    1.75 +  (P.comment >> (Toplevel.theory o IsarThy.add_subsubsection));
    1.76  
    1.77  
    1.78  (* classes and sorts *)
    1.79  
    1.80  val classesP =
    1.81 -  OuterSyntax.command "classes" "declare type classes"
    1.82 -    (Scan.repeat1 (name -- Scan.optional ($$$ "<" |-- !!! (list1 xname)) [])
    1.83 +  OuterSyntax.command "classes" "declare type classes" K.thy_decl
    1.84 +    (Scan.repeat1 (P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) [])
    1.85        >> (Toplevel.theory o Theory.add_classes));
    1.86  
    1.87  val classrelP =
    1.88 -  OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)"
    1.89 -    (xname -- ($$$ "<" |-- !!! xname) >> (Toplevel.theory o Theory.add_classrel o single));
    1.90 +  OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)" K.thy_decl
    1.91 +    (P.xname -- (P.$$$ "<" |-- P.!!! P.xname) >> (Toplevel.theory o Theory.add_classrel o single));
    1.92  
    1.93  val defaultsortP =
    1.94 -  OuterSyntax.command "defaultsort" "declare default sort"
    1.95 -    (sort >> (Toplevel.theory o Theory.add_defsort));
    1.96 +  OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
    1.97 +    (P.sort >> (Toplevel.theory o Theory.add_defsort));
    1.98  
    1.99  
   1.100  (* types *)
   1.101  
   1.102  val typedeclP =
   1.103 -  OuterSyntax.command "typedecl" "Pure type declaration"
   1.104 -    (type_args -- name -- opt_infix
   1.105 +  OuterSyntax.command "typedecl" "Pure type declaration" K.thy_decl
   1.106 +    (P.type_args -- P.name -- P.opt_infix
   1.107        >> (fn ((args, a), mx) => Toplevel.theory (PureThy.add_typedecls [(a, args, mx)])));
   1.108  
   1.109  val typeabbrP =
   1.110 -  OuterSyntax.command "types" "declare type abbreviations"
   1.111 -    (Scan.repeat1 (type_args -- name -- ($$$ "=" |-- !!! (typ -- opt_infix)))
   1.112 +  OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
   1.113 +    (Scan.repeat1 (P.type_args -- P.name -- (P.$$$ "=" |-- P.!!! (P.typ -- P.opt_infix)))
   1.114        >> (Toplevel.theory o Theory.add_tyabbrs o
   1.115          map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
   1.116  
   1.117  val nontermP =
   1.118    OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
   1.119 -    (Scan.repeat1 name >> (Toplevel.theory o Theory.add_nonterminals));
   1.120 +    K.thy_decl (Scan.repeat1 P.name >> (Toplevel.theory o Theory.add_nonterminals));
   1.121  
   1.122  val aritiesP =
   1.123 -  OuterSyntax.command "arities" "state type arities (axiomatic!)"
   1.124 -    (Scan.repeat1 (xname -- ($$$ "::" |-- !!! arity) >> triple2)
   1.125 +  OuterSyntax.command "arities" "state type arities (axiomatic!)" K.thy_decl
   1.126 +    (Scan.repeat1 (P.xname -- (P.$$$ "::" |-- P.!!! P.arity) >> P.triple2)
   1.127        >> (Toplevel.theory o Theory.add_arities));
   1.128  
   1.129  
   1.130  (* consts and syntax *)
   1.131  
   1.132  val constsP =
   1.133 -  OuterSyntax.command "consts" "declare constants"
   1.134 -    (Scan.repeat1 const >> (Toplevel.theory o Theory.add_consts));
   1.135 +  OuterSyntax.command "consts" "declare constants" K.thy_decl
   1.136 +    (Scan.repeat1 P.const >> (Toplevel.theory o Theory.add_consts));
   1.137  
   1.138  val opt_mode =
   1.139    Scan.optional
   1.140 -    ($$$ "(" |-- !!! (name -- Scan.optional ($$$ "output" >> K false) true --| $$$ ")"))
   1.141 +    (P.$$$ "(" |-- P.!!! (P.name -- Scan.optional (P.$$$ "output" >> K false) true --| P.$$$ ")"))
   1.142      ("", true);
   1.143  
   1.144  val syntaxP =
   1.145 -  OuterSyntax.command "syntax" "declare syntactic constants"
   1.146 -    (opt_mode -- Scan.repeat1 const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
   1.147 +  OuterSyntax.command "syntax" "declare syntactic constants" K.thy_decl
   1.148 +    (opt_mode -- Scan.repeat1 P.const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
   1.149  
   1.150  
   1.151  (* translations *)
   1.152  
   1.153  val trans_pat =
   1.154 -  Scan.optional ($$$ "(" |-- !!! (xname --| $$$ ")")) "logic" -- string;
   1.155 +  Scan.optional (P.$$$ "(" |-- P.!!! (P.xname --| P.$$$ ")")) "logic" -- P.string;
   1.156  
   1.157  fun trans_arrow toks =
   1.158 -  ($$$ "=>" >> K Syntax.ParseRule ||
   1.159 -    $$$ "<=" >> K Syntax.PrintRule ||
   1.160 -    $$$ "==" >> K Syntax.ParsePrintRule) toks;
   1.161 +  (P.$$$ "=>" >> K Syntax.ParseRule ||
   1.162 +    P.$$$ "<=" >> K Syntax.PrintRule ||
   1.163 +    P.$$$ "==" >> K Syntax.ParsePrintRule) toks;
   1.164  
   1.165  val trans_line =
   1.166 -  trans_pat -- !!! (trans_arrow -- trans_pat)
   1.167 +  trans_pat -- P.!!! (trans_arrow -- trans_pat)
   1.168      >> (fn (left, (arr, right)) => arr (left, right));
   1.169  
   1.170  val translationsP =
   1.171 -  OuterSyntax.command "translations" "declare syntax translation rules"
   1.172 +  OuterSyntax.command "translations" "declare syntax translation rules" K.thy_decl
   1.173      (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
   1.174  
   1.175  
   1.176  (* axioms and definitions *)
   1.177  
   1.178  val axiomsP =
   1.179 -  OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)"
   1.180 -    (Scan.repeat1 spec_name >> (Toplevel.theory o IsarThy.add_axioms));
   1.181 +  OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
   1.182 +    (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarThy.add_axioms));
   1.183  
   1.184  val defsP =
   1.185 -  OuterSyntax.command "defs" "define constants"
   1.186 -    (Scan.repeat1 spec_opt_name >> (Toplevel.theory o IsarThy.add_defs));
   1.187 +  OuterSyntax.command "defs" "define constants" K.thy_decl
   1.188 +    (Scan.repeat1 P.spec_opt_name >> (Toplevel.theory o IsarThy.add_defs));
   1.189  
   1.190  val constdefsP =
   1.191 -  OuterSyntax.command "constdefs" "declare and define constants"
   1.192 -    (Scan.repeat1 (const -- term) >> (Toplevel.theory o IsarThy.add_constdefs));
   1.193 +  OuterSyntax.command "constdefs" "declare and define constants" K.thy_decl
   1.194 +    (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o IsarThy.add_constdefs));
   1.195  
   1.196  
   1.197  (* theorems *)
   1.198  
   1.199 -val facts = opt_thm_name "=" -- xthms1;
   1.200 +val facts = P.opt_thm_name "=" -- P.xthms1;
   1.201  
   1.202  val theoremsP =
   1.203 -  OuterSyntax.command "theorems" "define theorems"
   1.204 +  OuterSyntax.command "theorems" "define theorems" K.thy_decl
   1.205      (facts >> (Toplevel.theory o IsarThy.have_theorems));
   1.206  
   1.207  val lemmasP =
   1.208 -  OuterSyntax.command "lemmas" "define lemmas"
   1.209 +  OuterSyntax.command "lemmas" "define lemmas" K.thy_decl
   1.210      (facts >> (Toplevel.theory o IsarThy.have_lemmas));
   1.211  
   1.212  
   1.213  (* name space entry path *)
   1.214  
   1.215  val globalP =
   1.216 -  OuterSyntax.command "global" "disable prefixing of theory name"
   1.217 +  OuterSyntax.command "global" "disable prefixing of theory name" K.thy_decl
   1.218      (Scan.succeed (Toplevel.theory PureThy.global_path));
   1.219  
   1.220  val localP =
   1.221 -  OuterSyntax.command "local" "enable prefixing of theory name"
   1.222 +  OuterSyntax.command "local" "enable prefixing of theory name" K.thy_decl
   1.223      (Scan.succeed (Toplevel.theory PureThy.local_path));
   1.224  
   1.225  val pathP =
   1.226 -  OuterSyntax.command "path" "modify name-space entry path"
   1.227 -    (xname >> (Toplevel.theory o Theory.add_path));
   1.228 +  OuterSyntax.command "path" "modify name-space entry path" K.thy_decl
   1.229 +    (P.xname >> (Toplevel.theory o Theory.add_path));
   1.230  
   1.231  
   1.232  (* use ML text *)
   1.233  
   1.234  val useP =
   1.235 -  OuterSyntax.command "use" "eval ML text from file"
   1.236 -    (name >> IsarCmd.use);
   1.237 +  OuterSyntax.command "use" "eval ML text from file" K.diag
   1.238 +    (P.name >> IsarCmd.use);
   1.239  
   1.240  val mlP =
   1.241 -  OuterSyntax.command "ML" "eval ML text"
   1.242 -    (text >> (fn txt => IsarCmd.use_mltext txt o IsarCmd.use_mltext_theory txt));
   1.243 +  OuterSyntax.command "ML" "eval ML text" K.diag
   1.244 +    (P.text >> (fn txt => IsarCmd.use_mltext txt o IsarCmd.use_mltext_theory txt));
   1.245  
   1.246  val setupP =
   1.247 -  OuterSyntax.command "setup" "apply ML theory transformer"
   1.248 -    (text >> (Toplevel.theory o IsarThy.use_setup));
   1.249 +  OuterSyntax.command "setup" "apply ML theory transformer" K.thy_decl
   1.250 +    (P.text >> (Toplevel.theory o IsarThy.use_setup));
   1.251  
   1.252  
   1.253  (* translation functions *)
   1.254  
   1.255  val parse_ast_translationP =
   1.256 -  OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
   1.257 -    (text >> (Toplevel.theory o IsarThy.parse_ast_translation));
   1.258 +  OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" K.thy_decl
   1.259 +    (P.text >> (Toplevel.theory o IsarThy.parse_ast_translation));
   1.260  
   1.261  val parse_translationP =
   1.262 -  OuterSyntax.command "parse_translation" "install parse translation functions"
   1.263 -    (text >> (Toplevel.theory o IsarThy.parse_translation));
   1.264 +  OuterSyntax.command "parse_translation" "install parse translation functions" K.thy_decl
   1.265 +    (P.text >> (Toplevel.theory o IsarThy.parse_translation));
   1.266  
   1.267  val print_translationP =
   1.268 -  OuterSyntax.command "print_translation" "install print translation functions"
   1.269 -    (text >> (Toplevel.theory o IsarThy.print_translation));
   1.270 +  OuterSyntax.command "print_translation" "install print translation functions" K.thy_decl
   1.271 +    (P.text >> (Toplevel.theory o IsarThy.print_translation));
   1.272  
   1.273  val typed_print_translationP =
   1.274    OuterSyntax.command "typed_print_translation" "install typed print translation functions"
   1.275 -    (text >> (Toplevel.theory o IsarThy.typed_print_translation));
   1.276 +    K.thy_decl (P.text >> (Toplevel.theory o IsarThy.typed_print_translation));
   1.277  
   1.278  val print_ast_translationP =
   1.279 -  OuterSyntax.command "print_ast_translation" "install print ast translation functions"
   1.280 -    (text >> (Toplevel.theory o IsarThy.print_ast_translation));
   1.281 +  OuterSyntax.command "print_ast_translation" "install print ast translation functions" K.thy_decl
   1.282 +    (P.text >> (Toplevel.theory o IsarThy.print_ast_translation));
   1.283  
   1.284  val token_translationP =
   1.285 -  OuterSyntax.command "token_translation" "install token translation functions"
   1.286 -    (text >> (Toplevel.theory o IsarThy.token_translation));
   1.287 +  OuterSyntax.command "token_translation" "install token translation functions" K.thy_decl
   1.288 +    (P.text >> (Toplevel.theory o IsarThy.token_translation));
   1.289  
   1.290  
   1.291  (* oracles *)
   1.292  
   1.293  val oracleP =
   1.294 -  OuterSyntax.command "oracle" "install oracle"
   1.295 -    (name -- text >> (Toplevel.theory o IsarThy.add_oracle));
   1.296 +  OuterSyntax.command "oracle" "install oracle" K.thy_decl
   1.297 +    (P.name -- P.text >> (Toplevel.theory o IsarThy.add_oracle));
   1.298  
   1.299  
   1.300  
   1.301 @@ -236,108 +236,108 @@
   1.302  
   1.303  (* statements *)
   1.304  
   1.305 -val is_props = $$$ "(" |-- !!! (Scan.repeat1 ($$$ "is" |-- prop) --| $$$ ")");
   1.306 -val propp = prop -- Scan.optional is_props [];
   1.307 -fun statement f = opt_thm_name ":" -- propp >> (fn ((x, y), z) => f x y z);
   1.308 +val is_props = P.$$$ "(" |-- P.!!! (Scan.repeat1 (P.$$$ "is" |-- P.prop) --| P.$$$ ")");
   1.309 +val propp = P.prop -- Scan.optional is_props [];
   1.310 +fun statement f = P.opt_thm_name ":" -- propp >> (fn ((x, y), z) => f x y z);
   1.311  
   1.312  val theoremP =
   1.313 -  OuterSyntax.command "theorem" "state theorem"
   1.314 +  OuterSyntax.command "theorem" "state theorem" K.thy_goal
   1.315      (statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   1.316  
   1.317  val lemmaP =
   1.318 -  OuterSyntax.command "lemma" "state lemma"
   1.319 +  OuterSyntax.command "lemma" "state lemma" K.thy_goal
   1.320      (statement IsarThy.lemma >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   1.321  
   1.322  val showP =
   1.323 -  OuterSyntax.command "show" "state local goal, solving current obligation"
   1.324 +  OuterSyntax.command "show" "state local goal, solving current obligation" K.prf_goal
   1.325      (statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof f));
   1.326  
   1.327  val haveP =
   1.328 -  OuterSyntax.command "have" "state local goal"
   1.329 +  OuterSyntax.command "have" "state local goal" K.prf_goal
   1.330      (statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));
   1.331  
   1.332  val thusP =
   1.333 -  OuterSyntax.command "thus" "abbreviates \"then show\""
   1.334 +  OuterSyntax.command "thus" "abbreviates \"then show\"" K.prf_goal
   1.335      (statement IsarThy.thus >> (fn f => Toplevel.print o Toplevel.proof f));
   1.336  
   1.337  val henceP =
   1.338 -  OuterSyntax.command "hence" "abbreviates \"then have\""
   1.339 +  OuterSyntax.command "hence" "abbreviates \"then have\"" K.prf_goal
   1.340      (statement IsarThy.hence >> (fn f => Toplevel.print o Toplevel.proof f));
   1.341  
   1.342  
   1.343  (* facts *)
   1.344  
   1.345  val thenP =
   1.346 -  OuterSyntax.command "then" "forward chaining"
   1.347 +  OuterSyntax.command "then" "forward chaining" K.prf_chain
   1.348      (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.chain));
   1.349  
   1.350  val fromP =
   1.351 -  OuterSyntax.command "from" "forward chaining from given facts"
   1.352 -    (xthms1 >> (fn x => Toplevel.print o Toplevel.proof (IsarThy.from_facts x)));
   1.353 +  OuterSyntax.command "from" "forward chaining from given facts" K.prf_chain
   1.354 +    (P.xthms1 >> (fn x => Toplevel.print o Toplevel.proof (IsarThy.from_facts x)));
   1.355  
   1.356  val factsP =
   1.357 -  OuterSyntax.command "note" "define facts"
   1.358 +  OuterSyntax.command "note" "define facts" K.prf_decl
   1.359      (facts >> (Toplevel.proof o IsarThy.have_facts));
   1.360  
   1.361  
   1.362  (* proof context *)
   1.363  
   1.364  val assumeP =
   1.365 -  OuterSyntax.command "assume" "assume propositions"
   1.366 -    (opt_thm_name ":" -- Scan.repeat1 propp >>
   1.367 +  OuterSyntax.command "assume" "assume propositions" K.prf_decl
   1.368 +    (P.opt_thm_name ":" -- Scan.repeat1 propp >>
   1.369        (fn ((x, y), z) => Toplevel.print o Toplevel.proof (IsarThy.assume x y z)));
   1.370  
   1.371  val fixP =
   1.372 -  OuterSyntax.command "fix" "fix variables (Skolem constants)"
   1.373 -    (Scan.repeat1 (name -- Scan.option ($$$ "::" |-- typ))
   1.374 +  OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_decl
   1.375 +    (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ))
   1.376        >> (fn xs => Toplevel.print o Toplevel.proof (IsarThy.fix xs)));
   1.377  
   1.378  val letP =
   1.379 -  OuterSyntax.command "let" "bind text variables"
   1.380 -    (and_list1 (enum1 "as" term -- ($$$ "=" |-- term))
   1.381 +  OuterSyntax.command "let" "bind text variables" K.prf_decl
   1.382 +    (P.and_list1 (P.enum1 "as" P.term -- (P.$$$ "=" |-- P.term))
   1.383        >> (fn bs => Toplevel.print o Toplevel.proof (IsarThy.match_bind bs)));
   1.384  
   1.385  
   1.386  (* proof structure *)
   1.387  
   1.388  val beginP =
   1.389 -  OuterSyntax.command "{{" "begin explicit proof block"
   1.390 +  OuterSyntax.command "{{" "begin explicit proof block" K.prf_block
   1.391      (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.begin_block));
   1.392  
   1.393  val endP =
   1.394 -  OuterSyntax.command "}}" "end explicit proof block"
   1.395 +  OuterSyntax.command "}}" "end explicit proof block" K.prf_block
   1.396      (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.end_block));
   1.397  
   1.398  val nextP =
   1.399 -  OuterSyntax.command "next" "enter next proof block"
   1.400 +  OuterSyntax.command "next" "enter next proof block" K.prf_block
   1.401      (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.next_block));
   1.402  
   1.403  
   1.404  (* end proof *)
   1.405  
   1.406  val kill_proofP =
   1.407 -  OuterSyntax.improper_command "kill_proof" "abort current proof"
   1.408 +  OuterSyntax.improper_command "kill_proof" "abort current proof" K.control
   1.409      (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
   1.410  
   1.411  val qed_withP =
   1.412 -  OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
   1.413 -    (Scan.option name -- Scan.option attribs -- Scan.option method
   1.414 +  OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes" K.qed
   1.415 +    (Scan.option P.name -- Scan.option P.attribs -- Scan.option P.method
   1.416        >> (uncurry IsarThy.global_qed_with));
   1.417  
   1.418  val qedP =
   1.419 -  OuterSyntax.command "qed" "conclude (sub-)proof"
   1.420 -    (Scan.option method >> IsarThy.qed);
   1.421 +  OuterSyntax.command "qed" "conclude (sub-)proof" K.qed
   1.422 +    (Scan.option P.method >> IsarThy.qed);
   1.423  
   1.424  val terminal_proofP =
   1.425 -  OuterSyntax.command "by" "terminal backward proof"
   1.426 -    (method >> IsarThy.terminal_proof)
   1.427 +  OuterSyntax.command "by" "terminal backward proof" K.qed
   1.428 +    (P.method >> IsarThy.terminal_proof)
   1.429  
   1.430  val immediate_proofP =
   1.431 -  OuterSyntax.command "." "immediate proof"
   1.432 +  OuterSyntax.command "." "immediate proof" K.qed
   1.433      (Scan.succeed IsarThy.immediate_proof);
   1.434  
   1.435  val default_proofP =
   1.436 -  OuterSyntax.command ".." "default proof"
   1.437 +  OuterSyntax.command ".." "default proof" K.qed
   1.438      (Scan.succeed IsarThy.default_proof);
   1.439  
   1.440  
   1.441 @@ -345,49 +345,49 @@
   1.442  
   1.443  val refineP =
   1.444    OuterSyntax.improper_command "refine" "unstructured backward proof step, ignoring facts"
   1.445 -    (method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
   1.446 +    K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
   1.447  
   1.448  val then_refineP =
   1.449    OuterSyntax.improper_command "then_refine" "unstructured backward proof step, using facts"
   1.450 -    (method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
   1.451 +    K.prf_script (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
   1.452  
   1.453  val proofP =
   1.454 -  OuterSyntax.command "proof" "backward proof"
   1.455 -    (Scan.option method >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
   1.456 +  OuterSyntax.command "proof" "backward proof" K.prf_block
   1.457 +    (Scan.option P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
   1.458  
   1.459  
   1.460  (* proof history *)
   1.461  
   1.462  val clear_undoP =
   1.463 -  OuterSyntax.improper_command "clear_undo" "clear undo information"
   1.464 +  OuterSyntax.improper_command "clear_undo" "clear undo information" K.control
   1.465      (Scan.succeed (Toplevel.print o IsarCmd.clear_undo));
   1.466  
   1.467  val undoP =
   1.468 -  OuterSyntax.improper_command "undo" "undo last command"
   1.469 +  OuterSyntax.improper_command "undo" "undo last command" K.control
   1.470      (Scan.succeed (Toplevel.print o IsarCmd.undo));
   1.471  
   1.472  val redoP =
   1.473 -  OuterSyntax.improper_command "redo" "redo last command"
   1.474 +  OuterSyntax.improper_command "redo" "redo last command" K.control
   1.475      (Scan.succeed (Toplevel.print o IsarCmd.redo));
   1.476  
   1.477  val undosP =
   1.478 -  OuterSyntax.improper_command "undos" "undo last commands"
   1.479 -    (nat >> (fn n => Toplevel.print o IsarCmd.undos n));
   1.480 +  OuterSyntax.improper_command "undos" "undo last commands" K.control
   1.481 +    (P.nat >> (fn n => Toplevel.print o IsarCmd.undos n));
   1.482  
   1.483  val backP =
   1.484 -  OuterSyntax.improper_command "back" "backtracking of proof command"
   1.485 +  OuterSyntax.improper_command "back" "backtracking of proof command" K.prf_script
   1.486      (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.back));
   1.487  
   1.488  val prevP =
   1.489 -  OuterSyntax.improper_command "prev" "previous proof state"
   1.490 +  OuterSyntax.improper_command "prev" "previous proof state" K.control
   1.491      (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.prev));
   1.492  
   1.493  val upP =
   1.494 -  OuterSyntax.improper_command "up" "upper proof state"
   1.495 +  OuterSyntax.improper_command "up" "upper proof state" K.control
   1.496      (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.up));
   1.497  
   1.498  val topP =
   1.499 -  OuterSyntax.improper_command "top" "to initial proof state"
   1.500 +  OuterSyntax.improper_command "top" "to initial proof state" K.control
   1.501      (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));
   1.502  
   1.503  
   1.504 @@ -395,101 +395,101 @@
   1.505  (** diagnostic commands (for interactive mode only) **)
   1.506  
   1.507  val print_commandsP =
   1.508 -  OuterSyntax.improper_command "help" "print outer syntax (global)"
   1.509 +  OuterSyntax.improper_command "help" "print outer syntax (global)" K.diag
   1.510      (Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));
   1.511  
   1.512  val print_theoryP =
   1.513 -  OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)"
   1.514 +  OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
   1.515      (Scan.succeed IsarCmd.print_theory);
   1.516  
   1.517  val print_syntaxP =
   1.518 -  OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)"
   1.519 +  OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)" K.diag
   1.520      (Scan.succeed IsarCmd.print_syntax);
   1.521  
   1.522  val print_theoremsP =
   1.523 -  OuterSyntax.improper_command "print_theorems" "print theorems known in this theory"
   1.524 +  OuterSyntax.improper_command "print_theorems" "print theorems known in this theory" K.diag
   1.525      (Scan.succeed IsarCmd.print_theorems);
   1.526  
   1.527  val print_attributesP =
   1.528 -  OuterSyntax.improper_command "print_attributes" "print attributes known in this theory"
   1.529 +  OuterSyntax.improper_command "print_attributes" "print attributes known in this theory" K.diag
   1.530      (Scan.succeed IsarCmd.print_attributes);
   1.531  
   1.532  val print_methodsP =
   1.533 -  OuterSyntax.improper_command "print_methods" "print methods known in this theory"
   1.534 +  OuterSyntax.improper_command "print_methods" "print methods known in this theory" K.diag
   1.535      (Scan.succeed IsarCmd.print_methods);
   1.536  
   1.537  val print_bindsP =
   1.538 -  OuterSyntax.improper_command "print_binds" "print term bindings of proof context"
   1.539 +  OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
   1.540      (Scan.succeed IsarCmd.print_binds);
   1.541  
   1.542  val print_lthmsP =
   1.543 -  OuterSyntax.improper_command "print_facts" "print local theorems of proof context"
   1.544 +  OuterSyntax.improper_command "print_facts" "print local theorems of proof context" K.diag
   1.545      (Scan.succeed IsarCmd.print_lthms);
   1.546  
   1.547  val print_thmsP =
   1.548 -  OuterSyntax.improper_command "thm" "print theorems" (xthm >> IsarCmd.print_thms);
   1.549 +  OuterSyntax.improper_command "thm" "print theorems" K.diag (P.xthm >> IsarCmd.print_thms);
   1.550  
   1.551  val print_propP =
   1.552 -  OuterSyntax.improper_command "prop" "read and print proposition"
   1.553 -    (term >> IsarCmd.print_prop);
   1.554 +  OuterSyntax.improper_command "prop" "read and print proposition" K.diag
   1.555 +    (P.term >> IsarCmd.print_prop);
   1.556  
   1.557  val print_termP =
   1.558 -  OuterSyntax.improper_command "term" "read and print term"
   1.559 -    (term >> IsarCmd.print_term);
   1.560 +  OuterSyntax.improper_command "term" "read and print term" K.diag
   1.561 +    (P.term >> IsarCmd.print_term);
   1.562  
   1.563  val print_typeP =
   1.564 -  OuterSyntax.improper_command "typ" "read and print type"
   1.565 -    (typ >> IsarCmd.print_type);
   1.566 +  OuterSyntax.improper_command "typ" "read and print type" K.diag
   1.567 +    (P.typ >> IsarCmd.print_type);
   1.568  
   1.569  
   1.570  
   1.571  (** system commands (for interactive mode only) **)
   1.572  
   1.573  val cdP =
   1.574 -  OuterSyntax.improper_command "cd" "change current working directory"
   1.575 -    (name >> IsarCmd.cd);
   1.576 +  OuterSyntax.improper_command "cd" "change current working directory" K.control
   1.577 +    (P.name >> IsarCmd.cd);
   1.578  
   1.579  val pwdP =
   1.580 -  OuterSyntax.improper_command "pwd" "print current working directory"
   1.581 +  OuterSyntax.improper_command "pwd" "print current working directory" K.diag
   1.582      (Scan.succeed IsarCmd.pwd);
   1.583  
   1.584  val use_thyP =
   1.585 -  OuterSyntax.improper_command "use_thy" "use theory file"
   1.586 -    (name >> IsarCmd.use_thy);
   1.587 +  OuterSyntax.improper_command "use_thy" "use theory file" K.diag
   1.588 +    (P.name >> IsarCmd.use_thy);
   1.589  
   1.590  val use_thy_onlyP =
   1.591 -  OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML"
   1.592 -    (name >> IsarCmd.use_thy_only);
   1.593 +  OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML" K.diag
   1.594 +    (P.name >> IsarCmd.use_thy_only);
   1.595  
   1.596  val update_thyP =
   1.597 -  OuterSyntax.improper_command "update_thy" "update theory file"
   1.598 -    (name >> IsarCmd.update_thy);
   1.599 +  OuterSyntax.improper_command "update_thy" "update theory file" K.diag
   1.600 +    (P.name >> IsarCmd.update_thy);
   1.601  
   1.602  val prP =
   1.603 -  OuterSyntax.improper_command "pr" "print current toplevel state"
   1.604 +  OuterSyntax.improper_command "pr" "print current toplevel state" K.diag
   1.605      (Scan.succeed (Toplevel.print o Toplevel.imperative (K ())));
   1.606  
   1.607  
   1.608 -val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
   1.609 +val opt_unit = Scan.optional (P.$$$ "(" -- P.$$$ ")" >> (K ())) ();
   1.610  
   1.611  val commitP =
   1.612 -  OuterSyntax.improper_command "commit" "commit current session to ML database"
   1.613 +  OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
   1.614      (opt_unit >> (K IsarCmd.use_commit));
   1.615  
   1.616  val quitP =
   1.617 -  OuterSyntax.improper_command "quit" "quit Isabelle"
   1.618 +  OuterSyntax.improper_command "quit" "quit Isabelle" K.control
   1.619      (opt_unit >> (K IsarCmd.quit));
   1.620  
   1.621  val exitP =
   1.622 -  OuterSyntax.improper_command "exit" "exit Isar loop"
   1.623 +  OuterSyntax.improper_command "exit" "exit Isar loop" K.control
   1.624      (Scan.succeed IsarCmd.exit);
   1.625  
   1.626  val restartP =
   1.627 -  OuterSyntax.improper_command "restart" "restart Isar loop"
   1.628 +  OuterSyntax.improper_command "restart" "restart Isar loop" K.control
   1.629      (Scan.succeed IsarCmd.restart);
   1.630  
   1.631  val breakP =
   1.632 -  OuterSyntax.improper_command "break" "discontinue excursion (keep current state)"
   1.633 +  OuterSyntax.improper_command "break" "discontinue excursion (keep current state)" K.control
   1.634      (Scan.succeed IsarCmd.break);
   1.635  
   1.636