moved use_mltext, use_mltext_theory, use_let, use_setup to context.ML;
authorwenzelm
Mon Mar 06 21:08:36 2000 +0100 (2000-03-06 ago)
changeset 8349611342539639
parent 8348 ebbbfdb35c84
child 8350 75aaee32893d
moved use_mltext, use_mltext_theory, use_let, use_setup to context.ML;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon Mar 06 21:08:15 2000 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon Mar 06 21:08:36 2000 +0100
     1.3 @@ -104,11 +104,11 @@
     1.4    Context.setmp (try Toplevel.theory_of state) ThyInfo.use name);
     1.5  
     1.6  (*passes changes of theory context*)
     1.7 -val use_mltext_theory = Toplevel.theory' o IsarThy.use_mltext_theory;
     1.8 +val use_mltext_theory = Toplevel.theory' o Context.use_mltext_theory;
     1.9  
    1.10  (*ignore result theory context*)
    1.11  fun use_mltext v txt = Toplevel.keep' (fn verb => fn state =>
    1.12 -  (IsarThy.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
    1.13 +  (Context.use_mltext txt (v andalso verb) (try Toplevel.theory_of state)));
    1.14  
    1.15  (*Note: commit is dynamically bound*)
    1.16  val use_commit = use_mltext false "commit();";
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Mar 06 21:08:15 2000 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Mar 06 21:08:36 2000 +0100
     2.3 @@ -223,7 +223,7 @@
     2.4  
     2.5  val setupP =
     2.6    OuterSyntax.command "setup" "apply ML theory setup" K.thy_decl
     2.7 -    (P.text >> (Toplevel.theory o IsarThy.use_setup));
     2.8 +    (P.text >> (Toplevel.theory o Context.use_setup));
     2.9  
    2.10  
    2.11  (* translation functions *)
     3.1 --- a/src/Pure/Isar/isar_thy.ML	Mon Mar 06 21:08:15 2000 +0100
     3.2 +++ b/src/Pure/Isar/isar_thy.ML	Mon Mar 06 21:08:36 2000 +0100
     3.3 @@ -141,9 +141,6 @@
     3.4      -> Toplevel.transition -> Toplevel.transition
     3.5    val finally_i: (thm list * Comment.interest) option * Comment.text
     3.6      -> Toplevel.transition -> Toplevel.transition
     3.7 -  val use_mltext: string -> bool -> theory option -> unit
     3.8 -  val use_mltext_theory: string -> bool -> theory -> theory
     3.9 -  val use_setup: string -> theory -> theory
    3.10    val parse_ast_translation: string -> theory -> theory
    3.11    val parse_translation: string -> theory -> theory
    3.12    val print_translation: string -> theory -> theory
    3.13 @@ -456,51 +453,37 @@
    3.14  end;
    3.15  
    3.16  
    3.17 -(* use ML text *)
    3.18 -
    3.19 -fun use_mltext txt verb opt_thy = Context.setmp opt_thy (use_text writeln verb) txt;
    3.20 -fun use_mltext_theory txt verb thy = #2 (Context.pass_theory thy (use_text writeln verb) txt);
    3.21 -
    3.22 -fun use_context txt = use_mltext_theory ("Context.>> (" ^ txt ^ ");") false;
    3.23 -
    3.24 -fun use_let name body txt =
    3.25 -  use_context ("let val " ^ name ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
    3.26 -
    3.27 -val use_setup =
    3.28 -  use_let "setup: (theory -> theory) list" "Library.apply setup";
    3.29 -
    3.30 -
    3.31  (* translation functions *)
    3.32  
    3.33  val parse_ast_translation =
    3.34 -  use_let "parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
    3.35 +  Context.use_let "parse_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
    3.36      "Theory.add_trfuns (parse_ast_translation, [], [], [])";
    3.37  
    3.38  val parse_translation =
    3.39 -  use_let "parse_translation: (string * (term list -> term)) list"
    3.40 +  Context.use_let "parse_translation: (string * (term list -> term)) list"
    3.41      "Theory.add_trfuns ([], parse_translation, [], [])";
    3.42  
    3.43  val print_translation =
    3.44 -  use_let "print_translation: (string * (term list -> term)) list"
    3.45 +  Context.use_let "print_translation: (string * (term list -> term)) list"
    3.46      "Theory.add_trfuns ([], [], print_translation, [])";
    3.47  
    3.48  val print_ast_translation =
    3.49 -  use_let "print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
    3.50 +  Context.use_let "print_ast_translation: (string * (Syntax.ast list -> Syntax.ast)) list"
    3.51      "Theory.add_trfuns ([], [], [], print_ast_translation)";
    3.52  
    3.53  val typed_print_translation =
    3.54 -  use_let "typed_print_translation: (string * (bool -> typ -> term list -> term)) list"
    3.55 +  Context.use_let "typed_print_translation: (string * (bool -> typ -> term list -> term)) list"
    3.56      "Theory.add_trfunsT typed_print_translation";
    3.57  
    3.58  val token_translation =
    3.59 -  use_let "token_translation: (string * string * (string -> string * int)) list"
    3.60 +  Context.use_let "token_translation: (string * string * (string -> string * int)) list"
    3.61      "Theory.add_tokentrfuns token_translation";
    3.62  
    3.63  
    3.64  (* add_oracle *)
    3.65  
    3.66  fun add_oracle ((name, txt), comment_ignore) =
    3.67 -  use_let
    3.68 +  Context.use_let
    3.69      "oracle: bstring * (Sign.sg * Object.T -> term)"
    3.70      "Theory.add_oracle oracle"
    3.71      ("(" ^ quote name ^ ", " ^ txt ^ ")");