diff -r eb07469a4cdd -r fa98145420e3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Aug 16 13:42:38 2005 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Aug 16 13:42:39 2005 +0200
@@ -10,21 +10,21 @@
 structure IsarSyn: ISAR_SYN =
 struct
 
-structure P = OuterParse and K = OuterSyntax.Keyword;
+structure P = OuterParse and K = OuterKeyword;
 
 
 (** init and exit **)
 
 val theoryP =
-  OuterSyntax.command "theory" "begin theory" K.thy_begin
+  OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
     (ThyHeader.args >> (Toplevel.print oo IsarThy.theory));
 
 val end_excursionP =
-  OuterSyntax.command "end" "end current excursion" K.thy_end
+  OuterSyntax.command "end" "end current excursion" (K.tag_theory K.thy_end)
     (Scan.succeed (Toplevel.print o Toplevel.exit));
 
 val contextP =
-  OuterSyntax.improper_command "context" "switch theory context" K.thy_switch
+  OuterSyntax.improper_command "context" "switch theory context" (K.tag_theory K.thy_switch)
     (P.name >> (Toplevel.print oo IsarThy.context));
 
 
@@ -55,20 +55,20 @@
   (P.position P.text >> IsarCmd.add_text_raw);
 
 val sectP = OuterSyntax.markup_command IsarOutput.Markup "sect" "formal comment (proof)"
-  K.prf_heading (P.position P.text >> IsarCmd.add_sect);
+  (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_sect);
 
 val subsectP = OuterSyntax.markup_command IsarOutput.Markup "subsect" "formal comment (proof)"
-  K.prf_heading (P.position P.text >> IsarCmd.add_subsect);
+  (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_subsect);
 
 val subsubsectP = OuterSyntax.markup_command IsarOutput.Markup "subsubsect"
-  "formal comment (proof)" K.prf_heading
+  "formal comment (proof)" (K.tag_proof K.prf_heading)
   (P.position P.text >> IsarCmd.add_subsubsect);
 
 val txtP = OuterSyntax.markup_command IsarOutput.MarkupEnv "txt" "formal comment (proof)"
-  K.prf_decl (P.position P.text >> IsarCmd.add_txt);
+  (K.tag_proof K.prf_decl) (P.position P.text >> IsarCmd.add_txt);
 
 val txt_rawP = OuterSyntax.markup_command IsarOutput.Verbatim "txt_raw"
-  "raw document preparation text (proof)" K.prf_decl
+  "raw document preparation text (proof)" (K.tag_proof K.prf_decl)
   (P.position P.text >> IsarCmd.add_txt_raw);
 
 
@@ -235,27 +235,27 @@
 (* use ML text *)
 
 val useP =
-  OuterSyntax.command "use" "eval ML text from file" K.diag
+  OuterSyntax.command "use" "eval ML text from file" (K.tag_ml K.diag)
     (P.path >> (Toplevel.no_timing oo IsarCmd.use));
 
 val mlP =
-  OuterSyntax.command "ML" "eval ML text (diagnostic)" K.diag
+  OuterSyntax.command "ML" "eval ML text (diagnostic)" (K.tag_ml K.diag)
     (P.text >> IsarCmd.use_mltext true);
 
 val ml_commandP =
-  OuterSyntax.command "ML_command" "eval ML text" K.diag
+  OuterSyntax.command "ML_command" "eval ML text" (K.tag_ml K.diag)
     (P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
 
 val ml_setupP =
-  OuterSyntax.command "ML_setup" "eval ML text (may change theory)" K.thy_decl
+  OuterSyntax.command "ML_setup" "eval ML text (may change theory)" (K.tag_ml K.thy_decl)
     (P.text >> IsarCmd.use_mltext_theory);
 
 val setupP =
-  OuterSyntax.command "setup" "apply ML theory setup" K.thy_decl
+  OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
     (P.text >> (Toplevel.theory o IsarThy.generic_setup));
 
 val method_setupP =
-  OuterSyntax.command "method_setup" "define proof method in ML" K.thy_decl
+  OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
     (((P.name -- P.!!! (P.$$$ "=" |-- P.text -- P.text) >> P.triple2))
       >> (Toplevel.theory o IsarThy.method_setup));
 
@@ -265,34 +265,40 @@
 val trfun = P.opt_keyword "advanced" -- P.text;
 
 val parse_ast_translationP =
-  OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" K.thy_decl
+  OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
+    (K.tag_ml K.thy_decl)
     (trfun >> (Toplevel.theory o IsarThy.parse_ast_translation));
 
 val parse_translationP =
-  OuterSyntax.command "parse_translation" "install parse translation functions" K.thy_decl
+  OuterSyntax.command "parse_translation" "install parse translation functions"
+    (K.tag_ml K.thy_decl)
     (trfun >> (Toplevel.theory o IsarThy.parse_translation));
 
 val print_translationP =
-  OuterSyntax.command "print_translation" "install print translation functions" K.thy_decl
+  OuterSyntax.command "print_translation" "install print translation functions"
+    (K.tag_ml K.thy_decl)
     (trfun >> (Toplevel.theory o IsarThy.print_translation));
 
 val typed_print_translationP =
   OuterSyntax.command "typed_print_translation" "install typed print translation functions"
-    K.thy_decl (trfun >> (Toplevel.theory o IsarThy.typed_print_translation));
+    (K.tag_ml K.thy_decl)
+    (trfun >> (Toplevel.theory o IsarThy.typed_print_translation));
 
 val print_ast_translationP =
-  OuterSyntax.command "print_ast_translation" "install print ast translation functions" K.thy_decl
+  OuterSyntax.command "print_ast_translation" "install print ast translation functions"
+    (K.tag_ml K.thy_decl)
     (trfun >> (Toplevel.theory o IsarThy.print_ast_translation));
 
 val token_translationP =
-  OuterSyntax.command "token_translation" "install token translation functions" K.thy_decl
+  OuterSyntax.command "token_translation" "install token translation functions"
+    (K.tag_ml K.thy_decl)
     (P.text >> (Toplevel.theory o IsarThy.token_translation));
 
 
 (* oracles *)
 
 val oracleP =
-  OuterSyntax.command "oracle" "declare oracle" K.thy_decl
+  OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
     (P.name -- (P.$$$ "(" |-- P.text --| P.$$$ ")" --| P.$$$ "=")
       -- P.text >> (Toplevel.theory o IsarThy.add_oracle o P.triple1));
 
@@ -329,7 +335,8 @@
 
 val interpretP =
   OuterSyntax.command "interpret"
-    "prove and register interpretation of locale expression in proof context" K.prf_goal
+    "prove and register interpretation of locale expression in proof context"
+    (K.tag_proof K.prf_goal)
     (P.opt_thm_name ":" -- P.locale_expr -- P.!!! opt_inst
       >> ((Toplevel.print oo Toplevel.proof) o IsarThy.register_locally));
 
@@ -355,19 +362,23 @@
 val corollaryP = gen_theorem Drule.corollaryK;
 
 val showP =
-  OuterSyntax.command "show" "state local goal, solving current obligation" K.prf_goal
+  OuterSyntax.command "show" "state local goal, solving current obligation"
+    (K.tag_proof K.prf_goal)
     (statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.show));
 
 val haveP =
-  OuterSyntax.command "have" "state local goal" K.prf_goal
+  OuterSyntax.command "have" "state local goal"
+    (K.tag_proof K.prf_goal)
     (statement >> ((Toplevel.print oo Toplevel.proof) o IsarThy.have));
 
 val thusP =
-  OuterSyntax.command "thus" "abbreviates \"then show\"" K.prf_goal
+  OuterSyntax.command "thus" "abbreviates \"then show\""
+    (K.tag_proof K.prf_goal)
     (statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.thus));
 
 val henceP =
-  OuterSyntax.command "hence" "abbreviates \"then have\"" K.prf_goal
+  OuterSyntax.command "hence" "abbreviates \"then have\""
+    (K.tag_proof K.prf_goal)
     (statement >> ((Toplevel.print oo Toplevel.proof) o IsarThy.hence));
 
 
@@ -376,54 +387,64 @@
 val facts = P.and_list1 P.xthms1;
 
 val thenP =
-  OuterSyntax.command "then" "forward chaining" K.prf_chain
+  OuterSyntax.command "then" "forward chaining"
+    (K.tag_proof K.prf_chain)
     (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.chain)));
 
 val fromP =
-  OuterSyntax.command "from" "forward chaining from given facts" K.prf_chain
+  OuterSyntax.command "from" "forward chaining from given facts"
+    (K.tag_proof K.prf_chain)
     (facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.from_facts)));
 
 val withP =
-  OuterSyntax.command "with" "forward chaining from given and current facts" K.prf_chain
+  OuterSyntax.command "with" "forward chaining from given and current facts"
+    (K.tag_proof K.prf_chain)
     (facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.with_facts)));
 
 val noteP =
-  OuterSyntax.command "note" "define facts" K.prf_decl
+  OuterSyntax.command "note" "define facts"
+    (K.tag_proof K.prf_decl)
     (name_facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.have_facts)));
 
 val usingP =
-  OuterSyntax.command "using" "augment goal facts" K.prf_decl
+  OuterSyntax.command "using" "augment goal facts"
+    (K.tag_proof K.prf_decl)
     (facts >> (Toplevel.print oo (Toplevel.proof o IsarThy.using_facts)));
 
 
 (* proof context *)
 
 val fixP =
-  OuterSyntax.command "fix" "fix local variables (Skolem constants)" K.prf_asm
+  OuterSyntax.command "fix" "fix local variables (Skolem constants)"
+    (K.tag_proof K.prf_asm)
     (vars >> (Toplevel.print oo (Toplevel.proof o IsarThy.fix)));
 
 val assumeP =
-  OuterSyntax.command "assume" "assume propositions" K.prf_asm
+  OuterSyntax.command "assume" "assume propositions"
+    (K.tag_proof K.prf_asm)
     (statement >> (Toplevel.print oo (Toplevel.proof o IsarThy.assume)));
 
 val presumeP =
-  OuterSyntax.command "presume" "assume propositions, to be established later" K.prf_asm
+  OuterSyntax.command "presume" "assume propositions, to be established later"
+    (K.tag_proof K.prf_asm)
     (statement >> (Toplevel.print oo (Toplevel.proof o IsarThy.presume)));
 
 val defP =
-  OuterSyntax.command "def" "local definition" K.prf_asm
+  OuterSyntax.command "def" "local definition"
+    (K.tag_proof K.prf_asm)
     (P.opt_thm_name ":" -- (P.name -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp))
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
 
 val obtainP =
   OuterSyntax.command "obtain" "generalized existence"
-    K.prf_asm_goal
+    (K.tag_proof K.prf_asm_goal)
     (Scan.optional
       (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ))
         --| P.$$$ "where") [] -- statement >> (Toplevel.print oo IsarThy.obtain));
 
 val letP =
-  OuterSyntax.command "let" "bind text variables" K.prf_decl
+  OuterSyntax.command "let" "bind text variables"
+    (K.tag_proof K.prf_decl)
     (P.and_list1 (P.enum1 "and" P.term -- (P.$$$ "=" |-- P.term))
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.let_bind)));
 
@@ -432,76 +453,92 @@
     P.xname >> rpair []) -- P.opt_attribs >> P.triple1;
 
 val caseP =
-  OuterSyntax.command "case" "invoke local context" K.prf_asm
+  OuterSyntax.command "case" "invoke local context"
+    (K.tag_proof K.prf_asm)
     (case_spec >> (Toplevel.print oo (Toplevel.proof o IsarThy.invoke_case)));
 
 
 (* proof structure *)
 
 val beginP =
-  OuterSyntax.command "{" "begin explicit proof block" K.prf_open
+  OuterSyntax.command "{" "begin explicit proof block"
+    (K.tag_proof K.prf_open)
     (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.begin_block)));
 
 val endP =
-  OuterSyntax.command "}" "end explicit proof block" K.prf_close
+  OuterSyntax.command "}" "end explicit proof block"
+    (K.tag_proof K.prf_close)
     (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.end_block)));
 
 val nextP =
-  OuterSyntax.command "next" "enter next proof block" K.prf_block
+  OuterSyntax.command "next" "enter next proof block"
+    (K.tag_proof K.prf_block)
     (Scan.succeed (Toplevel.print o (Toplevel.proof IsarThy.next_block)));
 
 
 (* end proof *)
 
 val qedP =
-  OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
+  OuterSyntax.command "qed" "conclude (sub-)proof"
+    (K.tag_proof K.qed_block)
     (Scan.option P.method >> (IsarThy.cond_print oo IsarThy.qed));
 
 val terminal_proofP =
-  OuterSyntax.command "by" "terminal backward proof" K.qed
+  OuterSyntax.command "by" "terminal backward proof"
+    (K.tag_proof K.qed)
     (P.method -- Scan.option P.method >> (IsarThy.cond_print oo IsarThy.terminal_proof));
 
 val default_proofP =
-  OuterSyntax.command ".." "default proof" K.qed
+  OuterSyntax.command ".." "default proof"
+    (K.tag_proof K.qed)
     (Scan.succeed (IsarThy.cond_print o IsarThy.default_proof));
 
 val immediate_proofP =
-  OuterSyntax.command "." "immediate proof" K.qed
+  OuterSyntax.command "." "immediate proof"
+    (K.tag_proof K.qed)
     (Scan.succeed (IsarThy.cond_print o IsarThy.immediate_proof));
 
 val done_proofP =
-  OuterSyntax.command "done" "done proof" K.qed
+  OuterSyntax.command "done" "done proof"
+    (K.tag_proof K.qed)
     (Scan.succeed (IsarThy.cond_print o IsarThy.done_proof));
 
 val skip_proofP =
-  OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
+  OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)"
+    (K.tag_proof K.qed)
     (Scan.succeed (IsarThy.cond_print o IsarThy.skip_proof));
 
 val forget_proofP =
-  OuterSyntax.command "oops" "forget proof" K.qed_global
+  OuterSyntax.command "oops" "forget proof"
+    (K.tag_proof K.qed_global)
     (Scan.succeed IsarThy.forget_proof);
 
 
 (* proof steps *)
 
 val deferP =
-  OuterSyntax.command "defer" "shuffle internal proof state" K.prf_script
+  OuterSyntax.command "defer" "shuffle internal proof state"
+    (K.tag_proof K.prf_script)
     (Scan.option P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.defer)));
 
 val preferP =
-  OuterSyntax.command "prefer" "shuffle internal proof state" K.prf_script
+  OuterSyntax.command "prefer" "shuffle internal proof state"
+    (K.tag_proof K.prf_script)
     (P.nat >> (Toplevel.print oo (Toplevel.proof o IsarThy.prefer)));
 
 val applyP =
-  OuterSyntax.command "apply" "initial refinement step (unstructured)" K.prf_script
+  OuterSyntax.command "apply" "initial refinement step (unstructured)"
+    (K.tag_proof K.prf_script)
     (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply)));
 
 val apply_endP =
-  OuterSyntax.command "apply_end" "terminal refinement (unstructured)" K.prf_script
+  OuterSyntax.command "apply_end" "terminal refinement (unstructured)"
+    (K.tag_proof K.prf_script)
     (P.method >> (Toplevel.print oo (Toplevel.proof o IsarThy.apply_end)));
 
 val proofP =
-  OuterSyntax.command "proof" "backward proof" K.prf_block
+  OuterSyntax.command "proof" "backward proof"
+    (K.tag_proof K.prf_block)
     (Scan.option P.method >> (fn m => Toplevel.print o
       Toplevel.actual_proof (IsarThy.proof m) o
       Toplevel.skip_proof (History.apply (fn i => i + 1))));
@@ -513,27 +550,32 @@
   Scan.option (P.$$$ "(" |-- P.!!! ((P.xthms1 --| P.$$$ ")")));
 
 val alsoP =
-  OuterSyntax.command "also" "combine calculation and current facts" K.prf_decl
+  OuterSyntax.command "also" "combine calculation and current facts"
+    (K.tag_proof K.prf_decl)
     (calc_args >> (IsarThy.cond_print oo IsarThy.also));
 
 val finallyP =
-  OuterSyntax.command "finally" "combine calculation and current facts, exhibit result" K.prf_chain
+  OuterSyntax.command "finally" "combine calculation and current facts, exhibit result"
+    (K.tag_proof K.prf_chain)
     (calc_args >> (IsarThy.cond_print oo IsarThy.finally));
 
 val moreoverP =
-  OuterSyntax.command "moreover" "augment calculation by current facts" K.prf_decl
+  OuterSyntax.command "moreover" "augment calculation by current facts"
+    (K.tag_proof K.prf_decl)
     (Scan.succeed (IsarThy.cond_print o IsarThy.moreover));
 
 val ultimatelyP =
   OuterSyntax.command "ultimately" "augment calculation by current facts, exhibit result"
-    K.prf_chain (Scan.succeed (IsarThy.cond_print o IsarThy.ultimately));
+    (K.tag_proof K.prf_chain)
+    (Scan.succeed (IsarThy.cond_print o IsarThy.ultimately));
 
 
 (* proof navigation *)
 
 val backP =
-  OuterSyntax.command "back" "backtracking of proof command" K.prf_script
-    (Scan.optional (P.$$$ "!" >> K true) false >> (Toplevel.print oo IsarCmd.back));
+  OuterSyntax.command "back" "backtracking of proof command"
+    (K.tag_proof K.prf_script)
+    (Scan.succeed (Toplevel.print o IsarCmd.back));
 
 
 (* history *)
@@ -590,7 +632,8 @@
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
 
 val print_theoremsP =
-  OuterSyntax.improper_command "print_theorems" "print theorems of this theory" K.diag
+  OuterSyntax.improper_command "print_theorems"
+      "print theorems of local theory or proof context" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_theorems));
 
 val print_localesP =
@@ -788,8 +831,8 @@
   outer_parse.ML, otherwise be prepared for unexpected errors*)
 
 val _ = OuterSyntax.add_keywords
- ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
-  "<=", "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes",
+ ["!", "!!", "%", "(", ")", "+", ",", "--", ":", "::", ";", "<", "<=",
+  "=", "==", "=>", "?", "[", "]", "advanced", "and", "assumes",
   "begin", "binder", "concl", "constrains", "defines", "files",
   "fixes", "imports", "in", "includes", "infix", "infixl", "infixr",
   "is", "notes", "open", "output", "overloaded", "shows", "structure",
@@ -833,10 +876,4 @@
   kill_thyP, display_draftsP, print_draftsP, prP, disable_prP,
   enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
 
-val _ = IsarOutput.add_hidden_commands [
-  "use", "ML", "ML_command", "ML_setup", "setup", "method_setup",
-  "parse_ast_translation", "parse_translation", "print_translation",
-  "typed_print_translation", "print_ast_translation",
-  "token_translation"];
-
 end;