# HG changeset patch # User wenzelm # Date 952373316 -3600 # Node ID 611342539639667f16b5fe111e8818a2e8941612 # Parent ebbbfdb35c848eb84f887896a34f5c52a3118125 moved use_mltext, use_mltext_theory, use_let, use_setup to context.ML; diff -r ebbbfdb35c84 -r 611342539639 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Mon Mar 06 21:08:15 2000 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Mon Mar 06 21:08:36 2000 +0100 @@ -104,11 +104,11 @@ Context.setmp (try Toplevel.theory_of state) ThyInfo.use name); (*passes changes of theory context*) -val use_mltext_theory = Toplevel.theory' o IsarThy.use_mltext_theory; +val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory; (*ignore result theory context*) fun use_mltext v txt = Toplevel.keep' (fn verb => fn state => - (IsarThy.use_mltext txt (v andalso verb) (try Toplevel.theory_of state))); + (Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state))); (*Note: commit is dynamically bound*) val use_commit = use_mltext false "commit();"; diff -r ebbbfdb35c84 -r 611342539639 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon Mar 06 21:08:15 2000 +0100 +++ b/src/Pure/Isar/isar_syn.ML Mon Mar 06 21:08:36 2000 +0100 @@ -223,7 +223,7 @@ val setupP = OuterSyntax.command "setup" "apply ML theory setup" K.thy_decl - (P.text >> (Toplevel.theory o IsarThy.use_setup)); + (P.text >> (Toplevel.theory o Context.use_setup)); (* translation functions *) diff -r ebbbfdb35c84 -r 611342539639 src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Mon Mar 06 21:08:15 2000 +0100 +++ b/src/Pure/Isar/isar_thy.ML Mon Mar 06 21:08:36 2000 +0100 @@ -141,9 +141,6 @@ -> Toplevel.transition -> Toplevel.transition val finally_i: (thm list * Comment.interest) option * Comment.text -> Toplevel.transition -> Toplevel.transition - val use_mltext: string -> bool -> theory option -> unit - val use_mltext_theory: string -> bool -> theory -> theory - val use_setup: string -> theory -> theory val parse_ast_translation: string -> theory -> theory val parse_translation: string -> theory -> theory val print_translation: string -> theory -> theory @@ -456,51 +453,37 @@ end; -(* use ML text *) - -fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text writeln verb) txt; -fun use_mltext_theory txt verb thy = #2 (Context.pass_theory thy (use_text writeln verb) txt); - -fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false; - -fun use_let name body txt = - use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end"); - -val use_setup = - use_let "setup: (theory -> theory) list" "Library.apply setup"; - - (* translation functions *) val parse_ast_translation = - use_let "parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list" + Context.use_let "parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list" "Theory.add_trfuns (parse_ast_translation, [], [], [])"; val parse_translation = - use_let "parse_translation: (string * (term list -> term)) list" + Context.use_let "parse_translation: (string * (term list -> term)) list" "Theory.add_trfuns ([], parse_translation, [], [])"; val print_translation = - use_let "print_translation: (string * (term list -> term)) list" + Context.use_let "print_translation: (string * (term list -> term)) list" "Theory.add_trfuns ([], [], print_translation, [])"; val print_ast_translation = - use_let "print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list" + Context.use_let "print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list" "Theory.add_trfuns ([], [], [], print_ast_translation)"; val typed_print_translation = - use_let "typed_print_translation: (string * (bool -> typ -> term list -> term)) list" + Context.use_let "typed_print_translation: (string * (bool -> typ -> term list -> term)) list" "Theory.add_trfunsT typed_print_translation"; val token_translation = - use_let "token_translation: (string * string * (string -> string * int)) list" + Context.use_let "token_translation: (string * string * (string -> string * int)) list" "Theory.add_tokentrfuns token_translation"; (* add_oracle *) fun add_oracle ((name, txt), comment_ignore) = - use_let + Context.use_let "oracle: bstring * (Sign.sg * Object.T -> term)" "Theory.add_oracle oracle" ("(" ^ quote name ^ ", " ^ txt ^ ")");