# HG changeset patch # User wenzelm # Date 962899908 -7200 # Node ID 798673f65f024cfadb2f61fe3f05a67b082605f9 # Parent 19029b7de03c134a9afaf194b7cc3251ddf294eb allow comment in more commands; diff -r 19029b7de03c -r 798673f65f02 doc-src/IsarRef/pure.tex --- 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} diff -r 19029b7de03c -r 798673f65f02 src/Pure/Isar/isar_cmd.ML --- 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 *) diff -r 19029b7de03c -r 798673f65f02 src/Pure/Isar/isar_syn.ML --- 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 *) diff -r 19029b7de03c -r 798673f65f02 src/Pure/Isar/isar_thy.ML --- 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 *)