allow comment in more commands;

--- a/doc-src/IsarRef/pure.tex	Thu Jul 06 18:11:15 2000 +0200
+++ b/doc-src/IsarRef/pure.tex	Thu Jul 06 18:11:48 2000 +0200
@@ -384,9 +384,9 @@
 \railterm{MLcommand}
 
 \begin{rail}
-  'use' name
+  'use' name comment?
   ;
-  ('ML' | MLcommand | MLsetup | 'setup') text
+  ('ML' | MLcommand | MLsetup | 'setup') text comment?
   ;
   methodsetup name '=' text text comment?
   ;
@@ -451,6 +451,29 @@
   \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
 \end{matharray}
 
+\railalias{parseasttranslation}{parse\_ast\_translation}
+\railterm{parseasttranslation}
+
+\railalias{parsetranslation}{parse\_translation}
+\railterm{parsetranslation}
+
+\railalias{printtranslation}{print\_translation}
+\railterm{printtranslation}
+
+\railalias{typedprinttranslation}{typed\_print\_translation}
+\railterm{typedprinttranslation}
+
+\railalias{printasttranslation}{print\_ast\_translation}
+\railterm{printasttranslation}
+
+\railalias{tokentranslation}{token\_translation}
+\railterm{tokentranslation}
+
+\begin{rail}
+  ( parseasttranslation | parsetranslation | printtranslation | typedprinttranslation |
+  printasttranslation | tokentranslation ) text comment?
+\end{rail}
+
 Syntax translation functions written in ML admit almost arbitrary
 manipulations of Isabelle's inner syntax.  Any of the above commands have a
 single \railqtoken{text} argument that refers to an ML expression of
@@ -1029,6 +1052,8 @@
   ;
   'prefer' nat comment?
   ;
+  'back' comment?
+  ;
 \end{rail}
 
 \begin{descr}

--- a/src/Pure/Isar/isar_cmd.ML	Thu Jul 06 18:11:15 2000 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Jul 06 18:11:48 2000 +0200
@@ -29,9 +29,11 @@
   val undo_theory: Toplevel.transition -> Toplevel.transition
   val undo: Toplevel.transition -> Toplevel.transition
   val kill: Toplevel.transition -> Toplevel.transition
-  val use: string -> Toplevel.transition -> Toplevel.transition
-  val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
-  val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition
+  val back: bool * Comment.text -> Toplevel.transition -> Toplevel.transition
+  val use: string * Comment.text -> Toplevel.transition -> Toplevel.transition
+  val use_mltext_theory: string * Comment.text -> Toplevel.transition -> Toplevel.transition
+  val use_mltext: bool -> string * Comment.text -> Toplevel.transition -> Toplevel.transition
+  val use_setup: string * Comment.text -> theory -> theory
   val use_commit: Toplevel.transition -> Toplevel.transition
   val cd: string -> Toplevel.transition -> Toplevel.transition
   val pwd: Toplevel.transition -> Toplevel.transition
@@ -120,21 +122,25 @@
 val undo = Toplevel.kill o undo_theory o undos_proof 1;
 val kill = Toplevel.kill o kill_proof;
 
+val back = Toplevel.proof o ProofHistory.back o Comment.ignore;
+
 
 (* use ML text *)
 
-fun use name = Toplevel.keep (fn state =>
+fun use (name, comment_ignore) = Toplevel.keep (fn state =>
   Context.setmp (try Toplevel.theory_of state) ThyInfo.use name);
 
 (*passes changes of theory context*)
-val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory;
+val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory o Comment.ignore;
 
 (*ignore result theory context*)
-fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
+fun use_mltext v (txt, comment_ignore) = Toplevel.keep' (fn verb => fn state =>
   (Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
 
+val use_setup = Context.use_setup o Comment.ignore;
+
 (*Note: commit is dynamically bound*)
-val use_commit = use_mltext false "commit();";
+val use_commit = use_mltext false ("commit();", Comment.none);
 
 
 (* current working directory *)

--- a/src/Pure/Isar/isar_syn.ML	Thu Jul 06 18:11:15 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 06 18:11:48 2000 +0200
@@ -211,23 +211,23 @@
 
 val useP =
   OuterSyntax.command "use" "eval ML text from file" K.diag
-    (P.name >> (Toplevel.no_timing oo IsarCmd.use));
+    (P.name -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.use));
 
 val mlP =
   OuterSyntax.command "ML" "eval ML text (diagnostic)" K.diag
-    (P.text >> IsarCmd.use_mltext true);
+    (P.text -- P.marg_comment >> IsarCmd.use_mltext true);
 
 val ml_commandP =
   OuterSyntax.command "ML_command" "eval ML text" K.diag
-    (P.text >> IsarCmd.use_mltext false);
+    (P.text -- P.marg_comment >> IsarCmd.use_mltext false);
 
 val ml_setupP =
   OuterSyntax.command "ML_setup" "eval ML text (may change theory)" K.thy_decl
-    (P.text >> IsarCmd.use_mltext_theory);
+    (P.text -- P.marg_comment >> IsarCmd.use_mltext_theory);
 
 val setupP =
   OuterSyntax.command "setup" "apply ML theory setup" K.thy_decl
-    (P.text >> (Toplevel.theory o Context.use_setup));
+    (P.text -- P.marg_comment >> (Toplevel.theory o IsarCmd.use_setup));
 
 val method_setupP =
   OuterSyntax.command "method_setup" "define proof method in ML" K.thy_decl
@@ -239,27 +239,27 @@
 
 val parse_ast_translationP =
   OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" K.thy_decl
-    (P.text >> (Toplevel.theory o IsarThy.parse_ast_translation));
+    (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.parse_ast_translation));
 
 val parse_translationP =
   OuterSyntax.command "parse_translation" "install parse translation functions" K.thy_decl
-    (P.text >> (Toplevel.theory o IsarThy.parse_translation));
+    (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.parse_translation));
 
 val print_translationP =
   OuterSyntax.command "print_translation" "install print translation functions" K.thy_decl
-    (P.text >> (Toplevel.theory o IsarThy.print_translation));
+    (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.print_translation));
 
 val typed_print_translationP =
   OuterSyntax.command "typed_print_translation" "install typed print translation functions"
-    K.thy_decl (P.text >> (Toplevel.theory o IsarThy.typed_print_translation));
+    K.thy_decl (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.typed_print_translation));
 
 val print_ast_translationP =
   OuterSyntax.command "print_ast_translation" "install print ast translation functions" K.thy_decl
-    (P.text >> (Toplevel.theory o IsarThy.print_ast_translation));
+    (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.print_ast_translation));
 
 val token_translationP =
   OuterSyntax.command "token_translation" "install token translation functions" K.thy_decl
-    (P.text >> (Toplevel.theory o IsarThy.token_translation));
+    (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.token_translation));
 
 
 (* oracles *)
@@ -453,8 +453,8 @@
 
 val backP =
   OuterSyntax.command "back" "backtracking of proof command" K.prf_script
-    (Scan.optional (P.$$$ "!" >> K true) false >>
-      (Toplevel.print oo (Toplevel.proof o ProofHistory.back)));
+    (Scan.optional (P.$$$ "!" >> K true) false -- P.marg_comment >>
+      (Toplevel.print oo IsarCmd.back));
 
 
 (* history *)

--- a/src/Pure/Isar/isar_thy.ML	Thu Jul 06 18:11:15 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Thu Jul 06 18:11:48 2000 +0200
@@ -151,12 +151,12 @@
     -> Toplevel.transition -> Toplevel.transition
   val moreover: Comment.text -> Toplevel.transition -> Toplevel.transition
   val ultimately: Comment.text -> Toplevel.transition -> Toplevel.transition
-  val parse_ast_translation: string -> theory -> theory
-  val parse_translation: string -> theory -> theory
-  val print_translation: string -> theory -> theory
-  val typed_print_translation: string -> theory -> theory
-  val print_ast_translation: string -> theory -> theory
-  val token_translation: string -> theory -> theory
+  val parse_ast_translation: string * Comment.text -> theory -> theory
+  val parse_translation: string * Comment.text -> theory -> theory
+  val print_translation: string * Comment.text -> theory -> theory
+  val typed_print_translation: string * Comment.text -> theory -> theory
+  val print_ast_translation: string * Comment.text -> theory -> theory
+  val token_translation: string * Comment.text -> theory -> theory
   val method_setup: (bstring * string * string) * Comment.text -> theory -> theory
   val add_oracle: (bstring * string) * Comment.text -> theory -> theory
   val begin_theory: string -> string list -> (string * bool) list -> theory
@@ -516,27 +516,27 @@
 
 val parse_ast_translation =
   Context.use_let "parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
-    "Theory.add_trfuns (parse_ast_translation, [], [], [])";
+    "Theory.add_trfuns (parse_ast_translation, [], [], [])" o Comment.ignore;
 
 val parse_translation =
   Context.use_let "parse_translation: (string * (term list -> term)) list"
-    "Theory.add_trfuns ([], parse_translation, [], [])";
+    "Theory.add_trfuns ([], parse_translation, [], [])" o Comment.ignore;
 
 val print_translation =
   Context.use_let "print_translation: (string * (term list -> term)) list"
-    "Theory.add_trfuns ([], [], print_translation, [])";
+    "Theory.add_trfuns ([], [], print_translation, [])" o Comment.ignore;
 
 val print_ast_translation =
   Context.use_let "print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
-    "Theory.add_trfuns ([], [], [], print_ast_translation)";
+    "Theory.add_trfuns ([], [], [], print_ast_translation)" o Comment.ignore;
 
 val typed_print_translation =
   Context.use_let "typed_print_translation: (string * (bool -> typ -> term list -> term)) list"
-    "Theory.add_trfunsT typed_print_translation";
+    "Theory.add_trfunsT typed_print_translation" o Comment.ignore;
 
 val token_translation =
   Context.use_let "token_translation: (string * string * (string -> string * int)) list"
-    "Theory.add_tokentrfuns token_translation";
+    "Theory.add_tokentrfuns token_translation" o Comment.ignore;
 
 
 (* add method *)