allow comment in more commands;
authorwenzelm
Thu Jul 06 18:11:48 2000 +0200 (2000-07-06 ago)
changeset 9273798673f65f02
parent 9272 19029b7de03c
child 9274 21c302a2fd9a
allow comment in more commands;
doc-src/IsarRef/pure.tex
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
     1.1 --- a/doc-src/IsarRef/pure.tex	Thu Jul 06 18:11:15 2000 +0200
     1.2 +++ b/doc-src/IsarRef/pure.tex	Thu Jul 06 18:11:48 2000 +0200
     1.3 @@ -384,9 +384,9 @@
     1.4  \railterm{MLcommand}
     1.5  
     1.6  \begin{rail}
     1.7 -  'use' name
     1.8 +  'use' name comment?
     1.9    ;
    1.10 -  ('ML' | MLcommand | MLsetup | 'setup') text
    1.11 +  ('ML' | MLcommand | MLsetup | 'setup') text comment?
    1.12    ;
    1.13    methodsetup name '=' text text comment?
    1.14    ;
    1.15 @@ -451,6 +451,29 @@
    1.16    \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
    1.17  \end{matharray}
    1.18  
    1.19 +\railalias{parseasttranslation}{parse\_ast\_translation}
    1.20 +\railterm{parseasttranslation}
    1.21 +
    1.22 +\railalias{parsetranslation}{parse\_translation}
    1.23 +\railterm{parsetranslation}
    1.24 +
    1.25 +\railalias{printtranslation}{print\_translation}
    1.26 +\railterm{printtranslation}
    1.27 +
    1.28 +\railalias{typedprinttranslation}{typed\_print\_translation}
    1.29 +\railterm{typedprinttranslation}
    1.30 +
    1.31 +\railalias{printasttranslation}{print\_ast\_translation}
    1.32 +\railterm{printasttranslation}
    1.33 +
    1.34 +\railalias{tokentranslation}{token\_translation}
    1.35 +\railterm{tokentranslation}
    1.36 +
    1.37 +\begin{rail}
    1.38 +  ( parseasttranslation | parsetranslation | printtranslation | typedprinttranslation |
    1.39 +  printasttranslation | tokentranslation ) text comment?
    1.40 +\end{rail}
    1.41 +
    1.42  Syntax translation functions written in ML admit almost arbitrary
    1.43  manipulations of Isabelle's inner syntax.  Any of the above commands have a
    1.44  single \railqtoken{text} argument that refers to an ML expression of
    1.45 @@ -1029,6 +1052,8 @@
    1.46    ;
    1.47    'prefer' nat comment?
    1.48    ;
    1.49 +  'back' comment?
    1.50 +  ;
    1.51  \end{rail}
    1.52  
    1.53  \begin{descr}
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Jul 06 18:11:15 2000 +0200
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Jul 06 18:11:48 2000 +0200
     2.3 @@ -29,9 +29,11 @@
     2.4    val undo_theory: Toplevel.transition -> Toplevel.transition
     2.5    val undo: Toplevel.transition -> Toplevel.transition
     2.6    val kill: Toplevel.transition -> Toplevel.transition
     2.7 -  val use: string -> Toplevel.transition -> Toplevel.transition
     2.8 -  val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
     2.9 -  val use_mltext: bool -> string -> Toplevel.transition -> Toplevel.transition
    2.10 +  val back: bool * Comment.text -> Toplevel.transition -> Toplevel.transition
    2.11 +  val use: string * Comment.text -> Toplevel.transition -> Toplevel.transition
    2.12 +  val use_mltext_theory: string * Comment.text -> Toplevel.transition -> Toplevel.transition
    2.13 +  val use_mltext: bool -> string * Comment.text -> Toplevel.transition -> Toplevel.transition
    2.14 +  val use_setup: string * Comment.text -> theory -> theory
    2.15    val use_commit: Toplevel.transition -> Toplevel.transition
    2.16    val cd: string -> Toplevel.transition -> Toplevel.transition
    2.17    val pwd: Toplevel.transition -> Toplevel.transition
    2.18 @@ -120,21 +122,25 @@
    2.19  val undo = Toplevel.kill o undo_theory o undos_proof 1;
    2.20  val kill = Toplevel.kill o kill_proof;
    2.21  
    2.22 +val back = Toplevel.proof o ProofHistory.back o Comment.ignore;
    2.23 +
    2.24  
    2.25  (* use ML text *)
    2.26  
    2.27 -fun use name = Toplevel.keep (fn state =>
    2.28 +fun use (name, comment_ignore) = Toplevel.keep (fn state =>
    2.29    Context.setmp (try Toplevel.theory_of state) ThyInfo.use name);
    2.30  
    2.31  (*passes changes of theory context*)
    2.32 -val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory;
    2.33 +val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory o Comment.ignore;
    2.34  
    2.35  (*ignore result theory context*)
    2.36 -fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
    2.37 +fun use_mltext v (txt, comment_ignore) = Toplevel.keep' (fn verb => fn state =>
    2.38    (Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
    2.39  
    2.40 +val use_setup = Context.use_setup o Comment.ignore;
    2.41 +
    2.42  (*Note: commit is dynamically bound*)
    2.43 -val use_commit = use_mltext false "commit();";
    2.44 +val use_commit = use_mltext false ("commit();", Comment.none);
    2.45  
    2.46  
    2.47  (* current working directory *)
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Jul 06 18:11:15 2000 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 06 18:11:48 2000 +0200
     3.3 @@ -211,23 +211,23 @@
     3.4  
     3.5  val useP =
     3.6    OuterSyntax.command "use" "eval ML text from file" K.diag
     3.7 -    (P.name >> (Toplevel.no_timing oo IsarCmd.use));
     3.8 +    (P.name -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.use));
     3.9  
    3.10  val mlP =
    3.11    OuterSyntax.command "ML" "eval ML text (diagnostic)" K.diag
    3.12 -    (P.text >> IsarCmd.use_mltext true);
    3.13 +    (P.text -- P.marg_comment >> IsarCmd.use_mltext true);
    3.14  
    3.15  val ml_commandP =
    3.16    OuterSyntax.command "ML_command" "eval ML text" K.diag
    3.17 -    (P.text >> IsarCmd.use_mltext false);
    3.18 +    (P.text -- P.marg_comment >> IsarCmd.use_mltext false);
    3.19  
    3.20  val ml_setupP =
    3.21    OuterSyntax.command "ML_setup" "eval ML text (may change theory)" K.thy_decl
    3.22 -    (P.text >> IsarCmd.use_mltext_theory);
    3.23 +    (P.text -- P.marg_comment >> IsarCmd.use_mltext_theory);
    3.24  
    3.25  val setupP =
    3.26    OuterSyntax.command "setup" "apply ML theory setup" K.thy_decl
    3.27 -    (P.text >> (Toplevel.theory o Context.use_setup));
    3.28 +    (P.text -- P.marg_comment >> (Toplevel.theory o IsarCmd.use_setup));
    3.29  
    3.30  val method_setupP =
    3.31    OuterSyntax.command "method_setup" "define proof method in ML" K.thy_decl
    3.32 @@ -239,27 +239,27 @@
    3.33  
    3.34  val parse_ast_translationP =
    3.35    OuterSyntax.command "parse_ast_translation" "install parse ast translation functions" K.thy_decl
    3.36 -    (P.text >> (Toplevel.theory o IsarThy.parse_ast_translation));
    3.37 +    (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.parse_ast_translation));
    3.38  
    3.39  val parse_translationP =
    3.40    OuterSyntax.command "parse_translation" "install parse translation functions" K.thy_decl
    3.41 -    (P.text >> (Toplevel.theory o IsarThy.parse_translation));
    3.42 +    (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.parse_translation));
    3.43  
    3.44  val print_translationP =
    3.45    OuterSyntax.command "print_translation" "install print translation functions" K.thy_decl
    3.46 -    (P.text >> (Toplevel.theory o IsarThy.print_translation));
    3.47 +    (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.print_translation));
    3.48  
    3.49  val typed_print_translationP =
    3.50    OuterSyntax.command "typed_print_translation" "install typed print translation functions"
    3.51 -    K.thy_decl (P.text >> (Toplevel.theory o IsarThy.typed_print_translation));
    3.52 +    K.thy_decl (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.typed_print_translation));
    3.53  
    3.54  val print_ast_translationP =
    3.55    OuterSyntax.command "print_ast_translation" "install print ast translation functions" K.thy_decl
    3.56 -    (P.text >> (Toplevel.theory o IsarThy.print_ast_translation));
    3.57 +    (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.print_ast_translation));
    3.58  
    3.59  val token_translationP =
    3.60    OuterSyntax.command "token_translation" "install token translation functions" K.thy_decl
    3.61 -    (P.text >> (Toplevel.theory o IsarThy.token_translation));
    3.62 +    (P.text -- P.marg_comment >> (Toplevel.theory o IsarThy.token_translation));
    3.63  
    3.64  
    3.65  (* oracles *)
    3.66 @@ -453,8 +453,8 @@
    3.67  
    3.68  val backP =
    3.69    OuterSyntax.command "back" "backtracking of proof command" K.prf_script
    3.70 -    (Scan.optional (P.$$$ "!" >> K true) false >>
    3.71 -      (Toplevel.print oo (Toplevel.proof o ProofHistory.back)));
    3.72 +    (Scan.optional (P.$$$ "!" >> K true) false -- P.marg_comment >>
    3.73 +      (Toplevel.print oo IsarCmd.back));
    3.74  
    3.75  
    3.76  (* history *)
     4.1 --- a/src/Pure/Isar/isar_thy.ML	Thu Jul 06 18:11:15 2000 +0200
     4.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Jul 06 18:11:48 2000 +0200
     4.3 @@ -151,12 +151,12 @@
     4.4      -> Toplevel.transition -> Toplevel.transition
     4.5    val moreover: Comment.text -> Toplevel.transition -> Toplevel.transition
     4.6    val ultimately: Comment.text -> Toplevel.transition -> Toplevel.transition
     4.7 -  val parse_ast_translation: string -> theory -> theory
     4.8 -  val parse_translation: string -> theory -> theory
     4.9 -  val print_translation: string -> theory -> theory
    4.10 -  val typed_print_translation: string -> theory -> theory
    4.11 -  val print_ast_translation: string -> theory -> theory
    4.12 -  val token_translation: string -> theory -> theory
    4.13 +  val parse_ast_translation: string * Comment.text -> theory -> theory
    4.14 +  val parse_translation: string * Comment.text -> theory -> theory
    4.15 +  val print_translation: string * Comment.text -> theory -> theory
    4.16 +  val typed_print_translation: string * Comment.text -> theory -> theory
    4.17 +  val print_ast_translation: string * Comment.text -> theory -> theory
    4.18 +  val token_translation: string * Comment.text -> theory -> theory
    4.19    val method_setup: (bstring * string * string) * Comment.text -> theory -> theory
    4.20    val add_oracle: (bstring * string) * Comment.text -> theory -> theory
    4.21    val begin_theory: string -> string list -> (string * bool) list -> theory
    4.22 @@ -516,27 +516,27 @@
    4.23  
    4.24  val parse_ast_translation =
    4.25    Context.use_let "parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
    4.26 -    "Theory.add_trfuns (parse_ast_translation, [], [], [])";
    4.27 +    "Theory.add_trfuns (parse_ast_translation, [], [], [])" o Comment.ignore;
    4.28  
    4.29  val parse_translation =
    4.30    Context.use_let "parse_translation: (string * (term list -> term)) list"
    4.31 -    "Theory.add_trfuns ([], parse_translation, [], [])";
    4.32 +    "Theory.add_trfuns ([], parse_translation, [], [])" o Comment.ignore;
    4.33  
    4.34  val print_translation =
    4.35    Context.use_let "print_translation: (string * (term list -> term)) list"
    4.36 -    "Theory.add_trfuns ([], [], print_translation, [])";
    4.37 +    "Theory.add_trfuns ([], [], print_translation, [])" o Comment.ignore;
    4.38  
    4.39  val print_ast_translation =
    4.40    Context.use_let "print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
    4.41 -    "Theory.add_trfuns ([], [], [], print_ast_translation)";
    4.42 +    "Theory.add_trfuns ([], [], [], print_ast_translation)" o Comment.ignore;
    4.43  
    4.44  val typed_print_translation =
    4.45    Context.use_let "typed_print_translation: (string * (bool -> typ -> term list -> term)) list"
    4.46 -    "Theory.add_trfunsT typed_print_translation";
    4.47 +    "Theory.add_trfunsT typed_print_translation" o Comment.ignore;
    4.48  
    4.49  val token_translation =
    4.50    Context.use_let "token_translation: (string * string * (string -> string * int)) list"
    4.51 -    "Theory.add_tokentrfuns token_translation";
    4.52 +    "Theory.add_tokentrfuns token_translation" o Comment.ignore;
    4.53  
    4.54  
    4.55  (* add method *)