moved ML_XXX.ML files to Pure/ML;
authorwenzelm
Fri Sep 14 17:02:34 2007 +0200 (2007-09-14)
changeset 24574e840872e9c7c
parent 24573 5bbdc9b60648
child 24575 8b5c5eb7df87
moved ML_XXX.ML files to Pure/ML;
src/Pure/General/ml_syntax.ML
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/ML/ml_context.ML
src/Pure/ML/ml_syntax.ML
src/Pure/ROOT.ML
src/Pure/Thy/ml_context.ML
     1.1 --- a/src/Pure/General/ml_syntax.ML	Fri Sep 14 15:27:12 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,96 +0,0 @@
     1.4 -(*  Title:      Pure/General/ml_syntax.ML
     1.5 -    ID:         $Id$
     1.6 -    Author:     Makarius
     1.7 -
     1.8 -Basic ML syntax operations.
     1.9 -*)
    1.10 -
    1.11 -signature ML_SYNTAX =
    1.12 -sig
    1.13 -  val reserved_names: string list
    1.14 -  val reserved: Name.context
    1.15 -  val is_reserved: string -> bool
    1.16 -  val is_identifier: string -> bool
    1.17 -  val atomic: string -> string
    1.18 -  val print_int: int -> string
    1.19 -  val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
    1.20 -  val print_list: ('a -> string) -> 'a list -> string
    1.21 -  val print_option: ('a -> string) -> 'a option -> string
    1.22 -  val print_char: string -> string
    1.23 -  val print_string: string -> string
    1.24 -  val print_strings: string list -> string
    1.25 -  val print_indexname: indexname -> string
    1.26 -  val print_class: class -> string
    1.27 -  val print_sort: sort -> string
    1.28 -  val print_typ: typ -> string
    1.29 -  val print_term: term -> string
    1.30 -end;
    1.31 -
    1.32 -structure ML_Syntax: ML_SYNTAX =
    1.33 -struct
    1.34 -
    1.35 -(* reserved words *)
    1.36 -
    1.37 -val reserved_names =
    1.38 - ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
    1.39 -  "end", "exception", "fn", "fun", "handle", "if", "in", "infix",
    1.40 -  "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse",
    1.41 -  "raise", "rec", "then", "type", "val", "with", "withtype", "while",
    1.42 -  "eqtype", "functor", "include", "sharing", "sig", "signature",
    1.43 -  "struct", "structure", "where"];
    1.44 -
    1.45 -val reserved = Name.make_context reserved_names;
    1.46 -val is_reserved = Name.is_declared reserved;
    1.47 -
    1.48 -
    1.49 -(* identifiers *)
    1.50 -
    1.51 -fun is_identifier name =
    1.52 -  not (is_reserved name) andalso Syntax.is_ascii_identifier name;
    1.53 -
    1.54 -
    1.55 -(* literal output -- unformatted *)
    1.56 -
    1.57 -val atomic = enclose "(" ")";
    1.58 -
    1.59 -val print_int = Int.toString;
    1.60 -
    1.61 -fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
    1.62 -
    1.63 -fun print_list f = enclose "[" "]" o commas o map f;
    1.64 -
    1.65 -fun print_option f NONE = "NONE"
    1.66 -  | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
    1.67 -
    1.68 -fun print_char s =
    1.69 -  if not (Symbol.is_char s) then raise Fail ("Bad character: " ^ quote s)
    1.70 -  else if s = "\"" then "\\\""
    1.71 -  else if s = "\\" then "\\\\"
    1.72 -  else
    1.73 -    let val c = ord s in
    1.74 -      if c < 32 then "\\^" ^ chr (c + ord "@")
    1.75 -      else if c < 127 then s
    1.76 -      else "\\" ^ string_of_int c
    1.77 -    end;
    1.78 -
    1.79 -val print_string = quote o translate_string print_char;
    1.80 -val print_strings = print_list print_string;
    1.81 -
    1.82 -val print_indexname = print_pair print_string print_int;
    1.83 -
    1.84 -val print_class = print_string;
    1.85 -val print_sort = print_list print_class;
    1.86 -
    1.87 -fun print_typ (Type arg) = "Type " ^ print_pair print_string (print_list print_typ) arg
    1.88 -  | print_typ (TFree arg) = "TFree " ^ print_pair print_string print_sort arg
    1.89 -  | print_typ (TVar arg) = "TVar " ^ print_pair print_indexname print_sort arg;
    1.90 -
    1.91 -fun print_term (Const arg) = "Const " ^ print_pair print_string print_typ arg
    1.92 -  | print_term (Free arg) = "Free " ^ print_pair print_string print_typ arg
    1.93 -  | print_term (Var arg) = "Var " ^ print_pair print_indexname print_typ arg
    1.94 -  | print_term (Bound i) = "Bound " ^ print_int i
    1.95 -  | print_term (Abs (s, T, t)) =
    1.96 -      "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
    1.97 -  | print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2);
    1.98 -
    1.99 -end;
     2.1 --- a/src/Pure/IsaMakefile	Fri Sep 14 15:27:12 2007 +0200
     2.2 +++ b/src/Pure/IsaMakefile	Fri Sep 14 17:02:34 2007 +0200
     2.3 @@ -27,33 +27,34 @@
     2.4    CPure.thy General/ROOT.ML General/alist.ML General/balanced_tree.ML		\
     2.5    General/basics.ML General/buffer.ML General/file.ML General/graph.ML		\
     2.6    General/heap.ML General/history.ML General/markup.ML				\
     2.7 -  General/ml_syntax.ML General/name_space.ML General/ord_list.ML		\
     2.8 -  General/output.ML General/path.ML General/position.ML				\
     2.9 -  General/pretty.ML General/print_mode.ML General/scan.ML			\
    2.10 -  General/secure.ML General/seq.ML General/source.ML General/stack.ML		\
    2.11 -  General/susp.ML General/symbol.ML General/table.ML General/url.ML		\
    2.12 -  General/xml.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML			\
    2.13 -  Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML Isar/code.ML		\
    2.14 -  Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML			\
    2.15 -  Isar/element.ML Isar/find_theorems.ML Isar/induct_attrib.ML			\
    2.16 -  Isar/isar_cmd.ML Isar/isar_syn.ML Isar/local_defs.ML				\
    2.17 -  Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML			\
    2.18 -  Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML		\
    2.19 -  Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML			\
    2.20 -  Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML			\
    2.21 -  Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML		\
    2.22 -  Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML				\
    2.23 -  Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML		\
    2.24 -  Isar/toplevel.ML ML-Systems/alice.ML ML-Systems/exn.ML			\
    2.25 +  General/name_space.ML General/ord_list.ML General/output.ML			\
    2.26 +  General/path.ML General/position.ML General/pretty.ML				\
    2.27 +  General/print_mode.ML General/scan.ML General/secure.ML General/seq.ML	\
    2.28 +  General/source.ML General/stack.ML General/susp.ML General/symbol.ML		\
    2.29 +  General/table.ML General/url.ML General/xml.ML Isar/ROOT.ML			\
    2.30 +  Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML		\
    2.31 +  Isar/calculation.ML Isar/class.ML Isar/code.ML Isar/code_unit.ML		\
    2.32 +  Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML			\
    2.33 +  Isar/find_theorems.ML Isar/induct_attrib.ML Isar/isar_cmd.ML			\
    2.34 +  Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML			\
    2.35 +  Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML		\
    2.36 +  Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML			\
    2.37 +  Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML			\
    2.38 +  Isar/proof.ML Isar/proof_context.ML Isar/proof_display.ML			\
    2.39 +  Isar/proof_history.ML Isar/rule_cases.ML Isar/rule_insts.ML			\
    2.40 +  Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML				\
    2.41 +  Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML			\
    2.42 +  ML-Systems/alice.ML ML-Systems/exn.ML						\
    2.43    ML-Systems/multithreading_dummy.ML ML-Systems/multithreading_polyml.ML	\
    2.44    ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML			\
    2.45    ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-5.0.ML				\
    2.46    ML-Systems/polyml-5.1.ML ML-Systems/polyml-interrupt-timeout.ML		\
    2.47    ML-Systems/polyml-old-basis.ML ML-Systems/polyml-posix.ML			\
    2.48    ML-Systems/polyml.ML ML-Systems/poplogml.ML ML-Systems/proper_int.ML		\
    2.49 -  ML-Systems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML		\
    2.50 -  Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML		\
    2.51 -  ProofGeneral/ROOT.ML ProofGeneral/parsing.ML ProofGeneral/pgip.ML		\
    2.52 +  ML-Systems/smlnj.ML ML/ml_context.ML ML/ml_syntax.ML				\
    2.53 +  Proof/extraction.ML Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML	\
    2.54 +  Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML		\
    2.55 +  ProofGeneral/parsing.ML ProofGeneral/pgip.ML					\
    2.56    ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML			\
    2.57    ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML			\
    2.58    ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML			\
    2.59 @@ -61,19 +62,19 @@
    2.60    ProofGeneral/proof_general_emacs.ML ProofGeneral/proof_general_pgip.ML	\
    2.61    Pure.thy ROOT.ML Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML		\
    2.62    Syntax/parser.ML Syntax/printer.ML Syntax/simple_syntax.ML			\
    2.63 -  Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML \
    2.64 -  Syntax/type_ext.ML Thy/html.ML Thy/latex.ML Thy/ml_context.ML			\
    2.65 -  Thy/present.ML Thy/term_style.ML Thy/thm_database.ML Thy/thm_deps.ML		\
    2.66 -  Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML		\
    2.67 -  Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML Tools/named_thms.ML		\
    2.68 -  Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML		\
    2.69 -  compress.ML config.ML conjunction.ML consts.ML context.ML			\
    2.70 -  context_position.ML conv.ML defs.ML display.ML drule.ML envir.ML		\
    2.71 -  fact_index.ML goal.ML library.ML logic.ML meta_simplifier.ML			\
    2.72 -  more_thm.ML morphism.ML name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML		\
    2.73 -  proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML	\
    2.74 -  sorts.ML subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML		\
    2.75 -  theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML
    2.76 +  Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML			\
    2.77 +  Syntax/type_ext.ML Thy/html.ML Thy/latex.ML Thy/present.ML			\
    2.78 +  Thy/term_style.ML Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_edit.ML		\
    2.79 +  Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_output.ML		\
    2.80 +  Tools/ROOT.ML Tools/invoke.ML Tools/named_thms.ML Tools/xml_syntax.ML		\
    2.81 +  assumption.ML axclass.ML codegen.ML compress.ML config.ML			\
    2.82 +  conjunction.ML consts.ML context.ML context_position.ML conv.ML		\
    2.83 +  defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML library.ML		\
    2.84 +  logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML		\
    2.85 +  old_goals.ML pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML		\
    2.86 +  pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML		\
    2.87 +  tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML		\
    2.88 +  type_infer.ML unify.ML variable.ML
    2.89  	@./mk
    2.90  
    2.91  
     3.1 --- a/src/Pure/Isar/ROOT.ML	Fri Sep 14 15:27:12 2007 +0200
     3.2 +++ b/src/Pure/Isar/ROOT.ML	Fri Sep 14 17:02:34 2007 +0200
     3.3 @@ -20,9 +20,9 @@
     3.4  use "outer_parse.ML";
     3.5  use "outer_keyword.ML";
     3.6  use "antiquote.ML";
     3.7 +use "../ML/ml_context.ML";
     3.8  
     3.9  (*theory sources*)
    3.10 -use "../Thy/ml_context.ML";
    3.11  use "../Thy/thy_header.ML";
    3.12  use "../Thy/thy_load.ML";
    3.13  use "../Thy/html.ML";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/ML/ml_context.ML	Fri Sep 14 17:02:34 2007 +0200
     4.3 @@ -0,0 +1,273 @@
     4.4 +(*  Title:      Pure/Thy/ml_context.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Makarius
     4.7 +
     4.8 +ML context and antiquotations.
     4.9 +*)
    4.10 +
    4.11 +signature BASIC_ML_CONTEXT =
    4.12 +sig
    4.13 +  val the_context: unit -> theory
    4.14 +  val thm: xstring -> thm
    4.15 +  val thms: xstring -> thm list
    4.16 +end;
    4.17 +
    4.18 +signature ML_CONTEXT =
    4.19 +sig
    4.20 +  include BASIC_ML_CONTEXT
    4.21 +  val get_context: unit -> Context.generic option
    4.22 +  val set_context: Context.generic option -> unit
    4.23 +  val setmp: Context.generic option -> ('a -> 'b) -> 'a -> 'b
    4.24 +  val the_generic_context: unit -> Context.generic
    4.25 +  val the_local_context: unit -> Proof.context
    4.26 +  val pass: Context.generic option -> ('a -> 'b) -> 'a -> 'b * Context.generic option
    4.27 +  val pass_context: Context.generic -> ('a -> 'b) -> 'a -> 'b * Context.generic
    4.28 +  val save: ('a -> 'b) -> 'a -> 'b
    4.29 +  val >> : (theory -> theory) -> unit
    4.30 +  val add_keywords: string list -> unit
    4.31 +  val inline_antiq: string ->
    4.32 +    (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
    4.33 +  val value_antiq: string ->
    4.34 +    (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit
    4.35 +  val proj_value_antiq: string -> (Context.generic * Args.T list ->
    4.36 +      (string * string * string) * (Context.generic * Args.T list)) -> unit
    4.37 +  val eval_antiquotes_fn: (string -> string * string) ref  (* FIXME tmp *)
    4.38 +  val trace: bool ref
    4.39 +  val use_mltext: string -> bool -> Context.generic option -> unit
    4.40 +  val use_mltext_update: string -> bool -> Context.generic -> Context.generic
    4.41 +  val use_let: string -> string -> string -> Context.generic -> Context.generic
    4.42 +  val use: Path.T -> unit
    4.43 +end;
    4.44 +
    4.45 +structure ML_Context: ML_CONTEXT =
    4.46 +struct
    4.47 +
    4.48 +(** Implicit ML context **)
    4.49 +
    4.50 +local
    4.51 +  val current_context = ref (NONE: Context.generic option);
    4.52 +in
    4.53 +  fun get_context () = ! current_context;
    4.54 +  fun set_context opt_context = current_context := opt_context;
    4.55 +  fun setmp opt_context f x = Library.setmp current_context opt_context f x;
    4.56 +end;
    4.57 +
    4.58 +fun the_generic_context () =
    4.59 +  (case get_context () of
    4.60 +    SOME context => context
    4.61 +  | _ => error "Unknown context");
    4.62 +
    4.63 +val the_local_context = Context.proof_of o the_generic_context;
    4.64 +
    4.65 +val the_context = Context.theory_of o the_generic_context;
    4.66 +
    4.67 +fun pass opt_context f x =
    4.68 +  setmp opt_context (fn x => let val y = f x in (y, get_context ()) end) x;
    4.69 +
    4.70 +fun pass_context context f x =
    4.71 +  (case pass (SOME context) f x of
    4.72 +    (y, SOME context') => (y, context')
    4.73 +  | (_, NONE) => error "Lost context in ML");
    4.74 +
    4.75 +fun save f x = CRITICAL (fn () => setmp (get_context ()) f x);
    4.76 +
    4.77 +fun change_theory f = CRITICAL (fn () =>
    4.78 +  set_context (SOME (Context.map_theory f (the_generic_context ()))));
    4.79 +
    4.80 +
    4.81 +
    4.82 +(** ML antiquotations **)
    4.83 +
    4.84 +(* maintain keywords *)
    4.85 +
    4.86 +val global_lexicon = ref Scan.empty_lexicon;
    4.87 +
    4.88 +fun add_keywords keywords = CRITICAL (fn () =>
    4.89 +  change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords)));
    4.90 +
    4.91 +
    4.92 +(* maintain commands *)
    4.93 +
    4.94 +datatype antiq = Inline of string | ProjValue of string * string * string;
    4.95 +val global_parsers = ref (Symtab.empty:
    4.96 +  (Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) Symtab.table);
    4.97 +
    4.98 +local
    4.99 +
   4.100 +fun add_item kind name scan = CRITICAL (fn () =>
   4.101 +  change global_parsers (fn tab =>
   4.102 +   (if not (Symtab.defined tab name) then ()
   4.103 +    else warning ("Redefined ML antiquotation: " ^ quote name);
   4.104 +    Symtab.update (name, scan >> kind) tab)));
   4.105 +
   4.106 +in
   4.107 +
   4.108 +val inline_antiq = add_item Inline;
   4.109 +val proj_value_antiq = add_item ProjValue;
   4.110 +fun value_antiq name scan = proj_value_antiq name (scan >> (fn (a, s) => (a, s, "")));
   4.111 +
   4.112 +end;
   4.113 +
   4.114 +
   4.115 +(* command syntax *)
   4.116 +
   4.117 +fun syntax scan src =
   4.118 +  #1 (Args.context_syntax "ML antiquotation" scan src (the_local_context ()));
   4.119 +
   4.120 +fun command src =
   4.121 +  let val ((name, _), pos) = Args.dest_src src in
   4.122 +    (case Symtab.lookup (! global_parsers) name of
   4.123 +      NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
   4.124 +    | SOME scan => syntax scan src)
   4.125 +  end;
   4.126 +
   4.127 +
   4.128 +(* outer syntax *)
   4.129 +
   4.130 +structure T = OuterLex;
   4.131 +structure P = OuterParse;
   4.132 +
   4.133 +val antiq =
   4.134 +  P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof)
   4.135 +  >> (fn ((x, pos), y) => Args.src ((x, y), pos));
   4.136 +
   4.137 +
   4.138 +(* input/output wrappers *)
   4.139 +
   4.140 +local
   4.141 +
   4.142 +val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;";
   4.143 +val isabelle_struct0 = isabelle_struct "";
   4.144 +
   4.145 +fun eval_antiquotes txt = CRITICAL (fn () =>
   4.146 +  let
   4.147 +    val ants = Antiquote.scan_antiquotes (txt, Position.line 1);
   4.148 +
   4.149 +    fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names)
   4.150 +      | expand (Antiquote.Antiq x) names =
   4.151 +          (case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of
   4.152 +            Inline s => (("", s), names)
   4.153 +          | ProjValue (a, s, f) =>
   4.154 +              let
   4.155 +                val a' = if ML_Syntax.is_identifier a then a else "val";
   4.156 +                val ([b], names') = Name.variants [a'] names;
   4.157 +                val binding = "val " ^ b ^ " = " ^ s ^ ";\n";
   4.158 +                val value =
   4.159 +                  if f = "" then "Isabelle." ^ b
   4.160 +                  else "(" ^ f ^ " Isabelle." ^ b ^ ")";
   4.161 +              in ((binding, value), names') end);
   4.162 +
   4.163 +    val (decls, body) =
   4.164 +      fold_map expand ants ML_Syntax.reserved
   4.165 +      |> #1 |> split_list |> pairself implode;
   4.166 +  in (isabelle_struct decls, body) end);
   4.167 +
   4.168 +fun eval name verbose txt = use_text name Output.ml_output verbose txt;
   4.169 +
   4.170 +in
   4.171 +
   4.172 +val eval_antiquotes_fn = ref eval_antiquotes;
   4.173 +
   4.174 +val trace = ref false;
   4.175 +
   4.176 +fun eval_wrapper name verbose txt =
   4.177 +  let
   4.178 +    val (txt1, txt2) = ! eval_antiquotes_fn txt;
   4.179 +    val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else ();
   4.180 +  in eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0 end;
   4.181 +
   4.182 +end;
   4.183 +
   4.184 +
   4.185 +(* ML evaluation *)
   4.186 +
   4.187 +fun use_mltext txt verbose opt_context =
   4.188 +  setmp opt_context (fn () => eval_wrapper "ML" verbose txt) ();
   4.189 +
   4.190 +fun use_mltext_update txt verbose context =
   4.191 +  #2 (pass_context context (eval_wrapper "ML" verbose) txt);
   4.192 +
   4.193 +fun use_context txt = use_mltext_update
   4.194 +  ("ML_Context.set_context (SOME ((" ^ txt ^ ") (ML_Context.the_generic_context ())));") false;
   4.195 +
   4.196 +fun use_let bind body txt =
   4.197 +  use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
   4.198 +
   4.199 +fun use path = eval_wrapper (Path.implode path) true (File.read path);
   4.200 +
   4.201 +
   4.202 +(* basic antiquotations *)
   4.203 +
   4.204 +val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()"));
   4.205 +
   4.206 +val _ = inline_antiq "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
   4.207 +val _ = inline_antiq "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
   4.208 +val _ = inline_antiq "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
   4.209 +
   4.210 +val _ = value_antiq "ctyp" (Args.typ >> (fn T =>
   4.211 +  ("ctyp",
   4.212 +    "Thm.ctyp_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))));
   4.213 +
   4.214 +val _ = value_antiq "cterm" (Args.term >> (fn t =>
   4.215 +  ("cterm",
   4.216 +    "Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))));
   4.217 +
   4.218 +val _ = value_antiq "cprop" (Args.prop >> (fn t =>
   4.219 +  ("cprop",
   4.220 +    "Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))));
   4.221 +
   4.222 +
   4.223 +fun const syn = (Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) =>
   4.224 +  #1 (Term.dest_Const (Consts.read_const (ProofContext.consts_of ctxt) c))
   4.225 +  |> syn ? ProofContext.const_syntax_name ctxt
   4.226 +  |> ML_Syntax.print_string);
   4.227 +
   4.228 +val _ = inline_antiq "const_name" (const false);
   4.229 +val _ = inline_antiq "const_syntax" (const true);
   4.230 +
   4.231 +
   4.232 +
   4.233 +(** fact references **)
   4.234 +
   4.235 +fun thm name = ProofContext.get_thm (the_local_context ()) (Name name);
   4.236 +fun thms name = ProofContext.get_thms (the_local_context ()) (Name name);
   4.237 +
   4.238 +
   4.239 +local
   4.240 +
   4.241 +fun print_interval (FromTo arg) =
   4.242 +      "PureThy.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg
   4.243 +  | print_interval (From i) = "PureThy.From " ^ ML_Syntax.print_int i
   4.244 +  | print_interval (Single i) = "PureThy.Single " ^ ML_Syntax.print_int i;
   4.245 +
   4.246 +fun thm_sel name =
   4.247 +  Args.thm_sel >> (fn is => "PureThy.NameSelection " ^
   4.248 +    ML_Syntax.print_pair ML_Syntax.print_string (ML_Syntax.print_list print_interval) (name, is))
   4.249 +  || Scan.succeed ("PureThy.Name " ^ ML_Syntax.print_string name);
   4.250 +
   4.251 +fun thm_antiq kind = value_antiq kind
   4.252 +  (Scan.lift (Args.name :-- thm_sel) >> apsnd (fn sel =>
   4.253 +    "ProofContext.get_" ^ kind ^ " (ML_Context.the_local_context ()) " ^ ML_Syntax.atomic sel));
   4.254 +
   4.255 +in
   4.256 +
   4.257 +val _ = add_keywords ["(", ")", "-", ","];
   4.258 +val _ = thm_antiq "thm";
   4.259 +val _ = thm_antiq "thms";
   4.260 +
   4.261 +end;
   4.262 +
   4.263 +val _ = proj_value_antiq "cpat" (Scan.lift Args.name >> 
   4.264 +      (fn ns => ("cpat", 
   4.265 +      "((cterm_of (ML_Context.the_context ())) o Library.the_single o " ^ 
   4.266 +      "(ProofContext.read_term_pats TypeInfer.logicT (ML_Context.the_local_context ())))"
   4.267 +      ^ (ML_Syntax.print_list ML_Syntax.print_string [ns]), "")));
   4.268 +
   4.269 +(*final declarations of this structure!*)
   4.270 +nonfix >>;
   4.271 +fun >> f = change_theory f;
   4.272 +
   4.273 +end;
   4.274 +
   4.275 +structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context;
   4.276 +open Basic_ML_Context;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/ML/ml_syntax.ML	Fri Sep 14 17:02:34 2007 +0200
     5.3 @@ -0,0 +1,96 @@
     5.4 +(*  Title:      Pure/General/ml_syntax.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Makarius
     5.7 +
     5.8 +Basic ML syntax operations.
     5.9 +*)
    5.10 +
    5.11 +signature ML_SYNTAX =
    5.12 +sig
    5.13 +  val reserved_names: string list
    5.14 +  val reserved: Name.context
    5.15 +  val is_reserved: string -> bool
    5.16 +  val is_identifier: string -> bool
    5.17 +  val atomic: string -> string
    5.18 +  val print_int: int -> string
    5.19 +  val print_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string
    5.20 +  val print_list: ('a -> string) -> 'a list -> string
    5.21 +  val print_option: ('a -> string) -> 'a option -> string
    5.22 +  val print_char: string -> string
    5.23 +  val print_string: string -> string
    5.24 +  val print_strings: string list -> string
    5.25 +  val print_indexname: indexname -> string
    5.26 +  val print_class: class -> string
    5.27 +  val print_sort: sort -> string
    5.28 +  val print_typ: typ -> string
    5.29 +  val print_term: term -> string
    5.30 +end;
    5.31 +
    5.32 +structure ML_Syntax: ML_SYNTAX =
    5.33 +struct
    5.34 +
    5.35 +(* reserved words *)
    5.36 +
    5.37 +val reserved_names =
    5.38 + ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
    5.39 +  "end", "exception", "fn", "fun", "handle", "if", "in", "infix",
    5.40 +  "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse",
    5.41 +  "raise", "rec", "then", "type", "val", "with", "withtype", "while",
    5.42 +  "eqtype", "functor", "include", "sharing", "sig", "signature",
    5.43 +  "struct", "structure", "where"];
    5.44 +
    5.45 +val reserved = Name.make_context reserved_names;
    5.46 +val is_reserved = Name.is_declared reserved;
    5.47 +
    5.48 +
    5.49 +(* identifiers *)
    5.50 +
    5.51 +fun is_identifier name =
    5.52 +  not (is_reserved name) andalso Syntax.is_ascii_identifier name;
    5.53 +
    5.54 +
    5.55 +(* literal output -- unformatted *)
    5.56 +
    5.57 +val atomic = enclose "(" ")";
    5.58 +
    5.59 +val print_int = Int.toString;
    5.60 +
    5.61 +fun print_pair f1 f2 (x, y) = "(" ^ f1 x ^ ", " ^ f2 y ^ ")";
    5.62 +
    5.63 +fun print_list f = enclose "[" "]" o commas o map f;
    5.64 +
    5.65 +fun print_option f NONE = "NONE"
    5.66 +  | print_option f (SOME x) = "SOME (" ^ f x ^ ")";
    5.67 +
    5.68 +fun print_char s =
    5.69 +  if not (Symbol.is_char s) then raise Fail ("Bad character: " ^ quote s)
    5.70 +  else if s = "\"" then "\\\""
    5.71 +  else if s = "\\" then "\\\\"
    5.72 +  else
    5.73 +    let val c = ord s in
    5.74 +      if c < 32 then "\\^" ^ chr (c + ord "@")
    5.75 +      else if c < 127 then s
    5.76 +      else "\\" ^ string_of_int c
    5.77 +    end;
    5.78 +
    5.79 +val print_string = quote o translate_string print_char;
    5.80 +val print_strings = print_list print_string;
    5.81 +
    5.82 +val print_indexname = print_pair print_string print_int;
    5.83 +
    5.84 +val print_class = print_string;
    5.85 +val print_sort = print_list print_class;
    5.86 +
    5.87 +fun print_typ (Type arg) = "Type " ^ print_pair print_string (print_list print_typ) arg
    5.88 +  | print_typ (TFree arg) = "TFree " ^ print_pair print_string print_sort arg
    5.89 +  | print_typ (TVar arg) = "TVar " ^ print_pair print_indexname print_sort arg;
    5.90 +
    5.91 +fun print_term (Const arg) = "Const " ^ print_pair print_string print_typ arg
    5.92 +  | print_term (Free arg) = "Free " ^ print_pair print_string print_typ arg
    5.93 +  | print_term (Var arg) = "Var " ^ print_pair print_indexname print_typ arg
    5.94 +  | print_term (Bound i) = "Bound " ^ print_int i
    5.95 +  | print_term (Abs (s, T, t)) =
    5.96 +      "Abs (" ^ print_string s ^ ", " ^ print_typ T ^ ", " ^ print_term t ^ ")"
    5.97 +  | print_term (t1 $ t2) = atomic (print_term t1) ^ " $ " ^ atomic (print_term t2);
    5.98 +
    5.99 +end;
     6.1 --- a/src/Pure/ROOT.ML	Fri Sep 14 15:27:12 2007 +0200
     6.2 +++ b/src/Pure/ROOT.ML	Fri Sep 14 17:02:34 2007 +0200
     6.3 @@ -44,7 +44,7 @@
     6.4  use "Syntax/printer.ML";
     6.5  use "Syntax/syntax.ML";
     6.6  
     6.7 -use "General/ml_syntax.ML";
     6.8 +use "ML/ml_syntax.ML";
     6.9  
    6.10  (*core of tactical proof system*)
    6.11  use "envir.ML";
     7.1 --- a/src/Pure/Thy/ml_context.ML	Fri Sep 14 15:27:12 2007 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,273 +0,0 @@
     7.4 -(*  Title:      Pure/Thy/ml_context.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Makarius
     7.7 -
     7.8 -ML context and antiquotations.
     7.9 -*)
    7.10 -
    7.11 -signature BASIC_ML_CONTEXT =
    7.12 -sig
    7.13 -  val the_context: unit -> theory
    7.14 -  val thm: xstring -> thm
    7.15 -  val thms: xstring -> thm list
    7.16 -end;
    7.17 -
    7.18 -signature ML_CONTEXT =
    7.19 -sig
    7.20 -  include BASIC_ML_CONTEXT
    7.21 -  val get_context: unit -> Context.generic option
    7.22 -  val set_context: Context.generic option -> unit
    7.23 -  val setmp: Context.generic option -> ('a -> 'b) -> 'a -> 'b
    7.24 -  val the_generic_context: unit -> Context.generic
    7.25 -  val the_local_context: unit -> Proof.context
    7.26 -  val pass: Context.generic option -> ('a -> 'b) -> 'a -> 'b * Context.generic option
    7.27 -  val pass_context: Context.generic -> ('a -> 'b) -> 'a -> 'b * Context.generic
    7.28 -  val save: ('a -> 'b) -> 'a -> 'b
    7.29 -  val >> : (theory -> theory) -> unit
    7.30 -  val add_keywords: string list -> unit
    7.31 -  val inline_antiq: string ->
    7.32 -    (Context.generic * Args.T list -> string * (Context.generic * Args.T list)) -> unit
    7.33 -  val value_antiq: string ->
    7.34 -    (Context.generic * Args.T list -> (string * string) * (Context.generic * Args.T list)) -> unit
    7.35 -  val proj_value_antiq: string -> (Context.generic * Args.T list ->
    7.36 -      (string * string * string) * (Context.generic * Args.T list)) -> unit
    7.37 -  val eval_antiquotes_fn: (string -> string * string) ref  (* FIXME tmp *)
    7.38 -  val trace: bool ref
    7.39 -  val use_mltext: string -> bool -> Context.generic option -> unit
    7.40 -  val use_mltext_update: string -> bool -> Context.generic -> Context.generic
    7.41 -  val use_let: string -> string -> string -> Context.generic -> Context.generic
    7.42 -  val use: Path.T -> unit
    7.43 -end;
    7.44 -
    7.45 -structure ML_Context: ML_CONTEXT =
    7.46 -struct
    7.47 -
    7.48 -(** Implicit ML context **)
    7.49 -
    7.50 -local
    7.51 -  val current_context = ref (NONE: Context.generic option);
    7.52 -in
    7.53 -  fun get_context () = ! current_context;
    7.54 -  fun set_context opt_context = current_context := opt_context;
    7.55 -  fun setmp opt_context f x = Library.setmp current_context opt_context f x;
    7.56 -end;
    7.57 -
    7.58 -fun the_generic_context () =
    7.59 -  (case get_context () of
    7.60 -    SOME context => context
    7.61 -  | _ => error "Unknown context");
    7.62 -
    7.63 -val the_local_context = Context.proof_of o the_generic_context;
    7.64 -
    7.65 -val the_context = Context.theory_of o the_generic_context;
    7.66 -
    7.67 -fun pass opt_context f x =
    7.68 -  setmp opt_context (fn x => let val y = f x in (y, get_context ()) end) x;
    7.69 -
    7.70 -fun pass_context context f x =
    7.71 -  (case pass (SOME context) f x of
    7.72 -    (y, SOME context') => (y, context')
    7.73 -  | (_, NONE) => error "Lost context in ML");
    7.74 -
    7.75 -fun save f x = CRITICAL (fn () => setmp (get_context ()) f x);
    7.76 -
    7.77 -fun change_theory f = CRITICAL (fn () =>
    7.78 -  set_context (SOME (Context.map_theory f (the_generic_context ()))));
    7.79 -
    7.80 -
    7.81 -
    7.82 -(** ML antiquotations **)
    7.83 -
    7.84 -(* maintain keywords *)
    7.85 -
    7.86 -val global_lexicon = ref Scan.empty_lexicon;
    7.87 -
    7.88 -fun add_keywords keywords = CRITICAL (fn () =>
    7.89 -  change global_lexicon (Scan.extend_lexicon (map Symbol.explode keywords)));
    7.90 -
    7.91 -
    7.92 -(* maintain commands *)
    7.93 -
    7.94 -datatype antiq = Inline of string | ProjValue of string * string * string;
    7.95 -val global_parsers = ref (Symtab.empty:
    7.96 -  (Context.generic * Args.T list -> antiq * (Context.generic * Args.T list)) Symtab.table);
    7.97 -
    7.98 -local
    7.99 -
   7.100 -fun add_item kind name scan = CRITICAL (fn () =>
   7.101 -  change global_parsers (fn tab =>
   7.102 -   (if not (Symtab.defined tab name) then ()
   7.103 -    else warning ("Redefined ML antiquotation: " ^ quote name);
   7.104 -    Symtab.update (name, scan >> kind) tab)));
   7.105 -
   7.106 -in
   7.107 -
   7.108 -val inline_antiq = add_item Inline;
   7.109 -val proj_value_antiq = add_item ProjValue;
   7.110 -fun value_antiq name scan = proj_value_antiq name (scan >> (fn (a, s) => (a, s, "")));
   7.111 -
   7.112 -end;
   7.113 -
   7.114 -
   7.115 -(* command syntax *)
   7.116 -
   7.117 -fun syntax scan src =
   7.118 -  #1 (Args.context_syntax "ML antiquotation" scan src (the_local_context ()));
   7.119 -
   7.120 -fun command src =
   7.121 -  let val ((name, _), pos) = Args.dest_src src in
   7.122 -    (case Symtab.lookup (! global_parsers) name of
   7.123 -      NONE => error ("Unknown ML antiquotation command: " ^ quote name ^ Position.str_of pos)
   7.124 -    | SOME scan => syntax scan src)
   7.125 -  end;
   7.126 -
   7.127 -
   7.128 -(* outer syntax *)
   7.129 -
   7.130 -structure T = OuterLex;
   7.131 -structure P = OuterParse;
   7.132 -
   7.133 -val antiq =
   7.134 -  P.!!! (P.position P.xname -- P.arguments --| Scan.ahead P.eof)
   7.135 -  >> (fn ((x, pos), y) => Args.src ((x, y), pos));
   7.136 -
   7.137 -
   7.138 -(* input/output wrappers *)
   7.139 -
   7.140 -local
   7.141 -
   7.142 -val isabelle_struct = enclose "structure Isabelle =\nstruct\n" "end;";
   7.143 -val isabelle_struct0 = isabelle_struct "";
   7.144 -
   7.145 -fun eval_antiquotes txt = CRITICAL (fn () =>
   7.146 -  let
   7.147 -    val ants = Antiquote.scan_antiquotes (txt, Position.line 1);
   7.148 -
   7.149 -    fun expand (Antiquote.Text s) names = (("", Symbol.escape s), names)
   7.150 -      | expand (Antiquote.Antiq x) names =
   7.151 -          (case command (Antiquote.scan_arguments (! global_lexicon) antiq x) of
   7.152 -            Inline s => (("", s), names)
   7.153 -          | ProjValue (a, s, f) =>
   7.154 -              let
   7.155 -                val a' = if ML_Syntax.is_identifier a then a else "val";
   7.156 -                val ([b], names') = Name.variants [a'] names;
   7.157 -                val binding = "val " ^ b ^ " = " ^ s ^ ";\n";
   7.158 -                val value =
   7.159 -                  if f = "" then "Isabelle." ^ b
   7.160 -                  else "(" ^ f ^ " Isabelle." ^ b ^ ")";
   7.161 -              in ((binding, value), names') end);
   7.162 -
   7.163 -    val (decls, body) =
   7.164 -      fold_map expand ants ML_Syntax.reserved
   7.165 -      |> #1 |> split_list |> pairself implode;
   7.166 -  in (isabelle_struct decls, body) end);
   7.167 -
   7.168 -fun eval name verbose txt = use_text name Output.ml_output verbose txt;
   7.169 -
   7.170 -in
   7.171 -
   7.172 -val eval_antiquotes_fn = ref eval_antiquotes;
   7.173 -
   7.174 -val trace = ref false;
   7.175 -
   7.176 -fun eval_wrapper name verbose txt =
   7.177 -  let
   7.178 -    val (txt1, txt2) = ! eval_antiquotes_fn txt;
   7.179 -    val _ = if ! trace then tracing (cat_lines [txt1, txt2]) else ();
   7.180 -  in eval "" false txt1; eval name verbose txt2; eval "" false isabelle_struct0 end;
   7.181 -
   7.182 -end;
   7.183 -
   7.184 -
   7.185 -(* ML evaluation *)
   7.186 -
   7.187 -fun use_mltext txt verbose opt_context =
   7.188 -  setmp opt_context (fn () => eval_wrapper "ML" verbose txt) ();
   7.189 -
   7.190 -fun use_mltext_update txt verbose context =
   7.191 -  #2 (pass_context context (eval_wrapper "ML" verbose) txt);
   7.192 -
   7.193 -fun use_context txt = use_mltext_update
   7.194 -  ("ML_Context.set_context (SOME ((" ^ txt ^ ") (ML_Context.the_generic_context ())));") false;
   7.195 -
   7.196 -fun use_let bind body txt =
   7.197 -  use_context ("let " ^ bind ^ " = " ^ txt ^ " in\n" ^ body ^ " end");
   7.198 -
   7.199 -fun use path = eval_wrapper (Path.implode path) true (File.read path);
   7.200 -
   7.201 -
   7.202 -(* basic antiquotations *)
   7.203 -
   7.204 -val _ = value_antiq "context" (Scan.succeed ("context", "ML_Context.the_local_context ()"));
   7.205 -
   7.206 -val _ = inline_antiq "typ" (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ));
   7.207 -val _ = inline_antiq "term" (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term));
   7.208 -val _ = inline_antiq "prop" (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term));
   7.209 -
   7.210 -val _ = value_antiq "ctyp" (Args.typ >> (fn T =>
   7.211 -  ("ctyp",
   7.212 -    "Thm.ctyp_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))));
   7.213 -
   7.214 -val _ = value_antiq "cterm" (Args.term >> (fn t =>
   7.215 -  ("cterm",
   7.216 -    "Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))));
   7.217 -
   7.218 -val _ = value_antiq "cprop" (Args.prop >> (fn t =>
   7.219 -  ("cprop",
   7.220 -    "Thm.cterm_of (ML_Context.the_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))));
   7.221 -
   7.222 -
   7.223 -fun const syn = (Scan.state >> Context.proof_of) -- Scan.lift Args.name >> (fn (ctxt, c) =>
   7.224 -  #1 (Term.dest_Const (Consts.read_const (ProofContext.consts_of ctxt) c))
   7.225 -  |> syn ? ProofContext.const_syntax_name ctxt
   7.226 -  |> ML_Syntax.print_string);
   7.227 -
   7.228 -val _ = inline_antiq "const_name" (const false);
   7.229 -val _ = inline_antiq "const_syntax" (const true);
   7.230 -
   7.231 -
   7.232 -
   7.233 -(** fact references **)
   7.234 -
   7.235 -fun thm name = ProofContext.get_thm (the_local_context ()) (Name name);
   7.236 -fun thms name = ProofContext.get_thms (the_local_context ()) (Name name);
   7.237 -
   7.238 -
   7.239 -local
   7.240 -
   7.241 -fun print_interval (FromTo arg) =
   7.242 -      "PureThy.FromTo " ^ ML_Syntax.print_pair ML_Syntax.print_int ML_Syntax.print_int arg
   7.243 -  | print_interval (From i) = "PureThy.From " ^ ML_Syntax.print_int i
   7.244 -  | print_interval (Single i) = "PureThy.Single " ^ ML_Syntax.print_int i;
   7.245 -
   7.246 -fun thm_sel name =
   7.247 -  Args.thm_sel >> (fn is => "PureThy.NameSelection " ^
   7.248 -    ML_Syntax.print_pair ML_Syntax.print_string (ML_Syntax.print_list print_interval) (name, is))
   7.249 -  || Scan.succeed ("PureThy.Name " ^ ML_Syntax.print_string name);
   7.250 -
   7.251 -fun thm_antiq kind = value_antiq kind
   7.252 -  (Scan.lift (Args.name :-- thm_sel) >> apsnd (fn sel =>
   7.253 -    "ProofContext.get_" ^ kind ^ " (ML_Context.the_local_context ()) " ^ ML_Syntax.atomic sel));
   7.254 -
   7.255 -in
   7.256 -
   7.257 -val _ = add_keywords ["(", ")", "-", ","];
   7.258 -val _ = thm_antiq "thm";
   7.259 -val _ = thm_antiq "thms";
   7.260 -
   7.261 -end;
   7.262 -
   7.263 -val _ = proj_value_antiq "cpat" (Scan.lift Args.name >> 
   7.264 -      (fn ns => ("cpat", 
   7.265 -      "((cterm_of (ML_Context.the_context ())) o Library.the_single o " ^ 
   7.266 -      "(ProofContext.read_term_pats TypeInfer.logicT (ML_Context.the_local_context ())))"
   7.267 -      ^ (ML_Syntax.print_list ML_Syntax.print_string [ns]), "")));
   7.268 -
   7.269 -(*final declarations of this structure!*)
   7.270 -nonfix >>;
   7.271 -fun >> f = change_theory f;
   7.272 -
   7.273 -end;
   7.274 -
   7.275 -structure Basic_ML_Context: BASIC_ML_CONTEXT = ML_Context;
   7.276 -open Basic_ML_Context;