merged, resolving conflict in src/Pure/Isar/attrib.ML;
authorwenzelm
Tue Jun 02 14:38:10 2009 +0200 (2009-06-02)
changeset 313657f65653e3d48
parent 31364 46da73330913
parent 31335 ba5b7749fa61
child 31367 8991eb94fb0b
merged, resolving conflict in src/Pure/Isar/attrib.ML;
src/Pure/Isar/attrib.ML
src/Pure/ML/ml_test.ML
     2.1 --- a/src/Pure/General/secure.ML	Tue Jun 02 14:00:24 2009 +0200
     2.2 +++ b/src/Pure/General/secure.ML	Tue Jun 02 14:38:10 2009 +0200
     2.3 @@ -9,6 +9,7 @@
     2.4    val set_secure: unit -> unit
     2.5    val is_secure: unit -> bool
     2.6    val deny_secure: string -> unit
     2.7 +  val secure_mltext: unit -> unit
     2.8    val use_text: use_context -> int * string -> bool -> string -> unit
     2.9    val use_file: use_context -> bool -> string -> unit
    2.10    val toplevel_pp: string list -> string -> unit
     3.1 --- a/src/Pure/IsaMakefile	Tue Jun 02 14:00:24 2009 +0200
     3.2 +++ b/src/Pure/IsaMakefile	Tue Jun 02 14:38:10 2009 +0200
     3.3 @@ -55,19 +55,20 @@
     3.4    General/table.ML General/url.ML General/xml.ML General/yxml.ML	\
     3.5    Isar/ROOT.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML		\
     3.6    Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML	\
     3.7 -  Isar/constdefs.ML Isar/context_rules.ML		\
     3.8 -  Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML			\
     3.9 -  Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML		\
    3.10 -  Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML		\
    3.11 -  Isar/method.ML Isar/object_logic.ML Isar/obtain.ML			\
    3.12 -  Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML		\
    3.13 -  Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML		\
    3.14 -  Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML	\
    3.15 -  Isar/rule_cases.ML Isar/rule_insts.ML Isar/skip_proof.ML		\
    3.16 -  Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML	\
    3.17 -  Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML		\
    3.18 -  ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML		\
    3.19 -  ML/ml_test.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML		\
    3.20 +  Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML		\
    3.21 +  Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML		\
    3.22 +  Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML		\
    3.23 +  Isar/local_theory.ML Isar/locale.ML Isar/method.ML			\
    3.24 +  Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML		\
    3.25 +  Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML		\
    3.26 +  Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML		\
    3.27 +  Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML		\
    3.28 +  Isar/rule_insts.ML Isar/skip_proof.ML Isar/spec_parse.ML		\
    3.29 +  Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML		\
    3.30 +  Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_compiler.ML		\
    3.31 +  ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML		\
    3.32 +  ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML		\
    3.33 +  ML-Systems/install_pp_polyml.ML					\
    3.34    ML-Systems/install_pp_polyml-experimental.ML				\
    3.35    ML-Systems/use_context.ML Proof/extraction.ML				\
    3.36    Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
     4.1 --- a/src/Pure/Isar/ROOT.ML	Tue Jun 02 14:00:24 2009 +0200
     4.2 +++ b/src/Pure/Isar/ROOT.ML	Tue Jun 02 14:38:10 2009 +0200
     4.3 @@ -24,6 +24,13 @@
     4.4  use "outer_parse.ML";
     4.5  use "value_parse.ML";
     4.6  use "args.ML";
     4.7 +
     4.8 +(*ML support*)
     4.9 +use "../ML/ml_syntax.ML";
    4.10 +use "../ML/ml_env.ML";
    4.11 +if ml_system = "polyml-experimental"
    4.12 +then use "../ML/ml_compiler_polyml-5.3.ML"
    4.13 +else use "../ML/ml_compiler.ML";
    4.14  use "../ML/ml_context.ML";
    4.15  
    4.16  (*theory sources*)
     5.1 --- a/src/Pure/Isar/attrib.ML	Tue Jun 02 14:00:24 2009 +0200
     5.2 +++ b/src/Pure/Isar/attrib.ML	Tue Jun 02 14:38:10 2009 +0200
     5.3 @@ -240,8 +240,7 @@
     5.4  
     5.5  (* rename_abs *)
     5.6  
     5.7 -val rename_abs : (Context.generic * thm -> Context.generic * thm) parser =
     5.8 -  Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars');
     5.9 +fun rename_abs x = (Scan.repeat (Args.maybe Args.name) >> (apsnd o Drule.rename_bvars')) x;
    5.10  
    5.11  
    5.12  (* unfold / fold definitions *)
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Jun 02 14:00:24 2009 +0200
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Jun 02 14:38:10 2009 +0200
     6.3 @@ -296,11 +296,11 @@
     6.4  (* use ML text *)
     6.5  
     6.6  fun propagate_env (context as Context.Proof lthy) =
     6.7 -      Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
     6.8 +      Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
     6.9    | propagate_env context = context;
    6.10  
    6.11  fun propagate_env_prf prf = Proof.map_contexts
    6.12 -  (Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf;
    6.13 +  (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
    6.14  
    6.15  val _ =
    6.16    OuterSyntax.command "use" "ML text from file" (K.tag_ml K.thy_decl)
     7.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Tue Jun 02 14:00:24 2009 +0200
     7.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Tue Jun 02 14:38:10 2009 +0200
     7.3 @@ -1,6 +1,6 @@
     7.4  (*  Title:      Pure/ML-Systems/compiler_polyml-5.0.ML
     7.5  
     7.6 -Runtime compilation -- for PolyML.compilerEx in version 5.0 and 5.1.
     7.7 +Runtime compilation for Poly/ML 5.0 and 5.1.
     7.8  *)
     7.9  
    7.10  fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
     8.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Tue Jun 02 14:00:24 2009 +0200
     8.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Tue Jun 02 14:38:10 2009 +0200
     8.3 @@ -17,6 +17,8 @@
     8.4  
     8.5  val forget_structure = PolyML.Compiler.forgetStructure;
     8.6  
     8.7 +val _ = PolyML.Compiler.forgetValue "print";
     8.8 +
     8.9  
    8.10  (* Compiler options *)
    8.11  
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Pure/ML/ml_compiler.ML	Tue Jun 02 14:38:10 2009 +0200
     9.3 @@ -0,0 +1,23 @@
     9.4 +(*  Title:      Pure/ML/ml_compiler.ML
     9.5 +    Author:     Makarius
     9.6 +
     9.7 +Runtime compilation -- generic version.
     9.8 +*)
     9.9 +
    9.10 +signature ML_COMPILER =
    9.11 +sig
    9.12 +  val eval: bool -> Position.T -> ML_Lex.token list -> unit
    9.13 +end
    9.14 +
    9.15 +structure ML_Compiler: ML_COMPILER =
    9.16 +struct
    9.17 +
    9.18 +fun eval verbose pos toks =
    9.19 +  let
    9.20 +    val line = the_default 1 (Position.line_of pos);
    9.21 +    val file = the_default "ML" (Position.file_of pos);
    9.22 +    val text = ML_Lex.flatten toks;
    9.23 +  in Secure.use_text ML_Env.local_context (line, file) verbose text end;
    9.24 +
    9.25 +end;
    9.26 +
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Jun 02 14:38:10 2009 +0200
    10.3 @@ -0,0 +1,144 @@
    10.4 +(*  Title:      Pure/ML/ml_compiler_polyml-5.3.ML
    10.5 +    Author:     Makarius
    10.6 +
    10.7 +Advanced runtime compilation for Poly/ML 5.3 (SVN 762).
    10.8 +*)
    10.9 +
   10.10 +signature ML_COMPILER =
   10.11 +sig
   10.12 +  val eval: bool -> Position.T -> ML_Lex.token list -> unit
   10.13 +end
   10.14 +
   10.15 +structure ML_Compiler: ML_COMPILER =
   10.16 +struct
   10.17 +
   10.18 +(* original source positions *)
   10.19 +
   10.20 +fun position_of (SOME context) (loc: PolyML.location) =
   10.21 +      (case pairself (ML_Env.token_position context) (#startPosition loc, #endPosition loc) of
   10.22 +        (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
   10.23 +      | (SOME pos, NONE) => pos
   10.24 +      | _ => Position.line_file (#startLine loc) (#file loc))
   10.25 +  | position_of NONE (loc: PolyML.location) = Position.line_file (#startLine loc) (#file loc);
   10.26 +
   10.27 +
   10.28 +(* parse trees *)
   10.29 +
   10.30 +fun report_parse_tree context depth space =
   10.31 +  let
   10.32 +    val pos_of = position_of context;
   10.33 +    fun report loc (PolyML.PTtype types) =
   10.34 +          PolyML.NameSpace.displayTypeExpression (types, depth, space)
   10.35 +          |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
   10.36 +          |> Position.report_text Markup.ML_typing (pos_of loc)
   10.37 +      | report loc (PolyML.PTdeclaredAt decl) =
   10.38 +          Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) ""
   10.39 +          |> Position.report_text Markup.ML_ref (pos_of loc)
   10.40 +      | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
   10.41 +      | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
   10.42 +      | report _ _ = ()
   10.43 +    and report_tree (loc, props) = List.app (report loc) props;
   10.44 +  in report_tree end;
   10.45 +
   10.46 +
   10.47 +(* eval ML source tokens *)
   10.48 +
   10.49 +fun eval verbose pos toks =
   10.50 +  let
   10.51 +    val _ = Secure.secure_mltext ();
   10.52 +    val {name_space = space, print, error = err, ...} = ML_Env.local_context;
   10.53 +
   10.54 +
   10.55 +    (* input *)
   10.56 +
   10.57 +    val input =
   10.58 +      if is_none (Context.thread_data ()) then map (pair 0) toks
   10.59 +      else Context.>>> (ML_Env.register_tokens toks);
   10.60 +    val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input);
   10.61 +
   10.62 +    val current_line = ref (the_default 1 (Position.line_of pos));
   10.63 +
   10.64 +    fun get_index () =
   10.65 +      the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer));
   10.66 +
   10.67 +    fun get () =
   10.68 +      (case ! input_buffer of
   10.69 +        [] => NONE
   10.70 +      | (_, []) :: rest => (input_buffer := rest; get ())
   10.71 +      | (i, c :: cs) :: rest =>
   10.72 +          (input_buffer := (i, cs) :: rest;
   10.73 +           if c = #"\n" then current_line := ! current_line + 1 else ();
   10.74 +           SOME c));
   10.75 +
   10.76 +
   10.77 +    (* output *)
   10.78 +
   10.79 +    val output_buffer = ref Buffer.empty;
   10.80 +    fun output () = Buffer.content (! output_buffer);
   10.81 +    fun put s = change output_buffer (Buffer.add s);
   10.82 +
   10.83 +    fun put_message {message, hard, location, context = _} =
   10.84 +     (put (if hard then "Error: " else "Warning: ");
   10.85 +      put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
   10.86 +      put (Position.str_of (position_of (Context.thread_data ()) location) ^ "\n"));
   10.87 +
   10.88 +
   10.89 +    (* results *)
   10.90 +
   10.91 +    val depth = get_print_depth ();
   10.92 +
   10.93 +    fun apply_result {fixes, types, signatures, structures, functors, values} =
   10.94 +      let
   10.95 +        fun display disp x =
   10.96 +          if depth > 0 then
   10.97 +            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
   10.98 +          else ();
   10.99 +
  10.100 +        fun apply_fix (a, b) =
  10.101 +          (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
  10.102 +        fun apply_type (a, b) =
  10.103 +          (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b));
  10.104 +        fun apply_sig (a, b) =
  10.105 +          (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
  10.106 +        fun apply_struct (a, b) =
  10.107 +          (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));
  10.108 +        fun apply_funct (a, b) =
  10.109 +          (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));
  10.110 +        fun apply_val (a, b) =
  10.111 +          (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));
  10.112 +      in
  10.113 +        List.app apply_fix fixes;
  10.114 +        List.app apply_type types;
  10.115 +        List.app apply_sig signatures;
  10.116 +        List.app apply_struct structures;
  10.117 +        List.app apply_funct functors;
  10.118 +        List.app apply_val values
  10.119 +      end;
  10.120 +
  10.121 +    fun result_fun (phase1, phase2) () =
  10.122 +     (case phase1 of NONE => ()
  10.123 +      | SOME parse_tree => report_parse_tree (Context.thread_data ()) depth space parse_tree;
  10.124 +      case phase2 of NONE => err "Static Errors"
  10.125 +      | SOME code => apply_result (code ()));  (* FIXME Toplevel.program *)
  10.126 +
  10.127 +
  10.128 +    (* compiler invocation *)
  10.129 +
  10.130 +    val parameters =
  10.131 +     [PolyML.Compiler.CPOutStream put,
  10.132 +      PolyML.Compiler.CPNameSpace space,
  10.133 +      PolyML.Compiler.CPErrorMessageProc put_message,
  10.134 +      PolyML.Compiler.CPLineNo (fn () => ! current_line),
  10.135 +      PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
  10.136 +      PolyML.Compiler.CPLineOffset get_index,
  10.137 +      PolyML.Compiler.CPCompilerResultFun result_fun];
  10.138 +    val _ =
  10.139 +      (while not (List.null (! input_buffer)) do
  10.140 +        PolyML.compiler (get, parameters) ())
  10.141 +      handle exn =>
  10.142 +       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
  10.143 +        err (output ()); raise exn);
  10.144 +  in if verbose then print (output ()) else () end;
  10.145 +
  10.146 +end;
  10.147 +
    11.1 --- a/src/Pure/ML/ml_context.ML	Tue Jun 02 14:00:24 2009 +0200
    11.2 +++ b/src/Pure/ML/ml_context.ML	Tue Jun 02 14:38:10 2009 +0200
    11.3 @@ -19,9 +19,6 @@
    11.4    val the_global_context: unit -> theory
    11.5    val the_local_context: unit -> Proof.context
    11.6    val exec: (unit -> unit) -> Context.generic -> Context.generic
    11.7 -  val inherit_env: Context.generic -> Context.generic -> Context.generic
    11.8 -  val name_space: ML_Name_Space.T
    11.9 -  val local_context: use_context
   11.10    val stored_thms: thm list ref
   11.11    val ml_store_thm: string * thm -> unit
   11.12    val ml_store_thms: string * thm list -> unit
   11.13 @@ -54,78 +51,6 @@
   11.14    | NONE => error "Missing context after execution");
   11.15  
   11.16  
   11.17 -(* ML name space *)
   11.18 -
   11.19 -structure ML_Env = GenericDataFun
   11.20 -(
   11.21 -  type T =
   11.22 -    ML_Name_Space.valueVal Symtab.table *
   11.23 -    ML_Name_Space.typeVal Symtab.table *
   11.24 -    ML_Name_Space.fixityVal Symtab.table *
   11.25 -    ML_Name_Space.structureVal Symtab.table *
   11.26 -    ML_Name_Space.signatureVal Symtab.table *
   11.27 -    ML_Name_Space.functorVal Symtab.table;
   11.28 -  val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
   11.29 -  val extend = I;
   11.30 -  fun merge _
   11.31 -   ((val1, type1, fixity1, structure1, signature1, functor1),
   11.32 -    (val2, type2, fixity2, structure2, signature2, functor2)) : T =
   11.33 -   (Symtab.merge (K true) (val1, val2),
   11.34 -    Symtab.merge (K true) (type1, type2),
   11.35 -    Symtab.merge (K true) (fixity1, fixity2),
   11.36 -    Symtab.merge (K true) (structure1, structure2),
   11.37 -    Symtab.merge (K true) (signature1, signature2),
   11.38 -    Symtab.merge (K true) (functor1, functor2));
   11.39 -);
   11.40 -
   11.41 -val inherit_env = ML_Env.put o ML_Env.get;
   11.42 -
   11.43 -val name_space: ML_Name_Space.T =
   11.44 -  let
   11.45 -    fun lookup sel1 sel2 name =
   11.46 -      Context.thread_data ()
   11.47 -      |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (ML_Env.get context)) name)
   11.48 -      |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
   11.49 -
   11.50 -    fun all sel1 sel2 () =
   11.51 -      Context.thread_data ()
   11.52 -      |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (ML_Env.get context)))
   11.53 -      |> append (sel2 ML_Name_Space.global ())
   11.54 -      |> sort_distinct (string_ord o pairself #1);
   11.55 -
   11.56 -    fun enter ap1 sel2 entry =
   11.57 -      if is_some (Context.thread_data ()) then
   11.58 -        Context.>> (ML_Env.map (ap1 (Symtab.update entry)))
   11.59 -      else sel2 ML_Name_Space.global entry;
   11.60 -  in
   11.61 -   {lookupVal    = lookup #1 #lookupVal,
   11.62 -    lookupType   = lookup #2 #lookupType,
   11.63 -    lookupFix    = lookup #3 #lookupFix,
   11.64 -    lookupStruct = lookup #4 #lookupStruct,
   11.65 -    lookupSig    = lookup #5 #lookupSig,
   11.66 -    lookupFunct  = lookup #6 #lookupFunct,
   11.67 -    enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
   11.68 -    enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
   11.69 -    enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
   11.70 -    enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
   11.71 -    enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
   11.72 -    enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
   11.73 -    allVal       = all #1 #allVal,
   11.74 -    allType      = all #2 #allType,
   11.75 -    allFix       = all #3 #allFix,
   11.76 -    allStruct    = all #4 #allStruct,
   11.77 -    allSig       = all #5 #allSig,
   11.78 -    allFunct     = all #6 #allFunct}
   11.79 -  end;
   11.80 -
   11.81 -val local_context: use_context =
   11.82 - {tune_source = ML_Parse.fix_ints,
   11.83 -  name_space = name_space,
   11.84 -  str_of_pos = Position.str_of oo Position.line_file,
   11.85 -  print = writeln,
   11.86 -  error = error};
   11.87 -
   11.88 -
   11.89  (* theorem bindings *)
   11.90  
   11.91  val stored_thms: thm list ref = ref [];
   11.92 @@ -139,8 +64,8 @@
   11.93        else if not (ML_Syntax.is_identifier name) then
   11.94          error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
   11.95        else setmp stored_thms ths' (fn () =>
   11.96 -        use_text local_context (0, "") true
   11.97 -          ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);")) ();
   11.98 +        ML_Compiler.eval true Position.none
   11.99 +          (ML_Lex.tokenize ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);"))) ();
  11.100    in () end;
  11.101  
  11.102  val ml_store_thms = ml_store "";
  11.103 @@ -199,6 +124,7 @@
  11.104  val struct_name = "Isabelle";
  11.105  val begin_env = ML_Lex.tokenize ("structure " ^ struct_name ^ " =\nstruct\n");
  11.106  val end_env = ML_Lex.tokenize "end;";
  11.107 +val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
  11.108  
  11.109  in
  11.110  
  11.111 @@ -240,26 +166,21 @@
  11.112  
  11.113  fun eval verbose pos txt =
  11.114    let
  11.115 -    fun eval_raw p = use_text local_context
  11.116 -      (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p));
  11.117 -
  11.118      (*prepare source text*)
  11.119      val _ = Position.report Markup.ML_source pos;
  11.120      val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
  11.121 -    val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ())
  11.122 -      |>> pairself (implode o map ML_Lex.text_of);
  11.123 -    val _ = if ! trace then tracing (cat_lines [env, body]) else ();
  11.124 +    val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
  11.125 +    val _ =
  11.126 +      if ! trace then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
  11.127 +      else ();
  11.128  
  11.129      (*prepare static ML environment*)
  11.130      val _ = Context.setmp_thread_data env_ctxt
  11.131 -        (fn () => (eval_raw Position.none false env; Context.thread_data ())) ()
  11.132 -      |> (fn NONE => () | SOME context' => Context.>> (inherit_env context'));
  11.133 +        (fn () => (ML_Compiler.eval false Position.none env; Context.thread_data ())) ()
  11.134 +      |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
  11.135  
  11.136 -    (*eval ML*)
  11.137 -    val _ = eval_raw pos verbose body;
  11.138 -
  11.139 -    (*reset static ML environment*)
  11.140 -    val _ = eval_raw Position.none false "structure Isabelle = struct end";
  11.141 +    val _ = ML_Compiler.eval verbose pos body;
  11.142 +    val _ = ML_Compiler.eval false Position.none reset_env;
  11.143    in () end;
  11.144  
  11.145  end;
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Pure/ML/ml_env.ML	Tue Jun 02 14:38:10 2009 +0200
    12.3 @@ -0,0 +1,111 @@
    12.4 +(*  Title:      Pure/ML/ml_env.ML
    12.5 +    Author:     Makarius
    12.6 +
    12.7 +Local environment of ML sources and results.
    12.8 +*)
    12.9 +
   12.10 +signature ML_ENV =
   12.11 +sig
   12.12 +  val inherit: Context.generic -> Context.generic -> Context.generic
   12.13 +  val register_tokens: ML_Lex.token list -> Context.generic ->
   12.14 +    (serial * ML_Lex.token) list * Context.generic
   12.15 +  val token_position: Context.generic -> serial -> Position.T option
   12.16 +  val name_space: ML_Name_Space.T
   12.17 +  val local_context: use_context
   12.18 +end
   12.19 +
   12.20 +structure ML_Env: ML_ENV =
   12.21 +struct
   12.22 +
   12.23 +(* context data *)
   12.24 +
   12.25 +structure Env = GenericDataFun
   12.26 +(
   12.27 +  type T =
   12.28 +    Position.T Inttab.table *
   12.29 +     (ML_Name_Space.valueVal Symtab.table *
   12.30 +      ML_Name_Space.typeVal Symtab.table *
   12.31 +      ML_Name_Space.fixityVal Symtab.table *
   12.32 +      ML_Name_Space.structureVal Symtab.table *
   12.33 +      ML_Name_Space.signatureVal Symtab.table *
   12.34 +      ML_Name_Space.functorVal Symtab.table);
   12.35 +  val empty =
   12.36 +    (Inttab.empty,
   12.37 +      (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
   12.38 +  val extend = I;
   12.39 +  fun merge _
   12.40 +   ((toks1, (val1, type1, fixity1, structure1, signature1, functor1)),
   12.41 +    (toks2, (val2, type2, fixity2, structure2, signature2, functor2))) : T =
   12.42 +   (Inttab.merge (K true) (toks1, toks2),
   12.43 +    (Symtab.merge (K true) (val1, val2),
   12.44 +     Symtab.merge (K true) (type1, type2),
   12.45 +     Symtab.merge (K true) (fixity1, fixity2),
   12.46 +     Symtab.merge (K true) (structure1, structure2),
   12.47 +     Symtab.merge (K true) (signature1, signature2),
   12.48 +     Symtab.merge (K true) (functor1, functor2)));
   12.49 +);
   12.50 +
   12.51 +val inherit = Env.put o Env.get;
   12.52 +
   12.53 +
   12.54 +(* source tokens *)
   12.55 +
   12.56 +fun register_tokens toks context =
   12.57 +  let
   12.58 +    val regs = map (fn tok => (serial (), tok)) toks;
   12.59 +    val context' = context
   12.60 +      |> Env.map (apfst (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs));
   12.61 +  in (regs, context') end;
   12.62 +
   12.63 +val token_position = Inttab.lookup o #1 o Env.get;
   12.64 +
   12.65 +
   12.66 +(* results *)
   12.67 +
   12.68 +val name_space: ML_Name_Space.T =
   12.69 +  let
   12.70 +    fun lookup sel1 sel2 name =
   12.71 +      Context.thread_data ()
   12.72 +      |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name)
   12.73 +      |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
   12.74 +
   12.75 +    fun all sel1 sel2 () =
   12.76 +      Context.thread_data ()
   12.77 +      |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (Env.get context))))
   12.78 +      |> append (sel2 ML_Name_Space.global ())
   12.79 +      |> sort_distinct (string_ord o pairself #1);
   12.80 +
   12.81 +    fun enter ap1 sel2 entry =
   12.82 +      if is_some (Context.thread_data ()) then
   12.83 +        Context.>> (Env.map (apsnd (ap1 (Symtab.update entry))))
   12.84 +      else sel2 ML_Name_Space.global entry;
   12.85 +  in
   12.86 +   {lookupVal    = lookup #1 #lookupVal,
   12.87 +    lookupType   = lookup #2 #lookupType,
   12.88 +    lookupFix    = lookup #3 #lookupFix,
   12.89 +    lookupStruct = lookup #4 #lookupStruct,
   12.90 +    lookupSig    = lookup #5 #lookupSig,
   12.91 +    lookupFunct  = lookup #6 #lookupFunct,
   12.92 +    enterVal     = enter (fn h => fn (a, b, c, d, e, f) => (h a, b, c, d, e, f)) #enterVal,
   12.93 +    enterType    = enter (fn h => fn (a, b, c, d, e, f) => (a, h b, c, d, e, f)) #enterType,
   12.94 +    enterFix     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, h c, d, e, f)) #enterFix,
   12.95 +    enterStruct  = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, h d, e, f)) #enterStruct,
   12.96 +    enterSig     = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, h e, f)) #enterSig,
   12.97 +    enterFunct   = enter (fn h => fn (a, b, c, d, e, f) => (a, b, c, d, e, h f)) #enterFunct,
   12.98 +    allVal       = all #1 #allVal,
   12.99 +    allType      = all #2 #allType,
  12.100 +    allFix       = all #3 #allFix,
  12.101 +    allStruct    = all #4 #allStruct,
  12.102 +    allSig       = all #5 #allSig,
  12.103 +    allFunct     = all #6 #allFunct}
  12.104 +  end;
  12.105 +
  12.106 +val local_context: use_context =
  12.107 + {tune_source = ML_Parse.fix_ints,
  12.108 +  name_space = name_space,
  12.109 +  str_of_pos = Position.str_of oo Position.line_file,
  12.110 +  print = writeln,
  12.111 +  error = error};
  12.112 +
  12.113 +end;
  12.114 +
    13.1 --- a/src/Pure/ML/ml_lex.ML	Tue Jun 02 14:00:24 2009 +0200
    13.2 +++ b/src/Pure/ML/ml_lex.ML	Tue Jun 02 14:38:10 2009 +0200
    13.3 @@ -18,6 +18,7 @@
    13.4    val kind_of: token -> token_kind
    13.5    val content_of: token -> string
    13.6    val text_of: token -> string
    13.7 +  val flatten: token list -> string
    13.8    val report_token: token -> unit
    13.9    val keywords: string list
   13.10    val source: (Symbol.symbol, 'a) Source.source ->
   13.11 @@ -73,6 +74,8 @@
   13.12      Error msg => error msg
   13.13    | _ => Symbol.escape (content_of tok));
   13.14  
   13.15 +val flatten = implode o map text_of;
   13.16 +
   13.17  fun is_regular (Token (_, (Error _, _))) = false
   13.18    | is_regular (Token (_, (EOF, _))) = false
   13.19    | is_regular _ = true;
    14.1 --- a/src/Pure/ML/ml_test.ML	Tue Jun 02 14:00:24 2009 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,191 +0,0 @@
    14.4 -(*  Title:      Pure/ML/ml_test.ML
    14.5 -    Author:     Makarius
    14.6 -
    14.7 -Test of advanced ML compiler invocation in Poly/ML 5.3 (SVN 744).
    14.8 -*)
    14.9 -
   14.10 -signature ML_TEST =
   14.11 -sig
   14.12 -  val position_of: Proof.context -> PolyML.location -> Position.T
   14.13 -  val eval: bool -> Position.T -> ML_Lex.token list -> unit
   14.14 -end
   14.15 -
   14.16 -structure ML_Test: ML_TEST =
   14.17 -struct
   14.18 -
   14.19 -(* extra ML environment *)
   14.20 -
   14.21 -structure Extra_Env = GenericDataFun
   14.22 -(
   14.23 -  type T = Position.T Inttab.table;  (*position of registered tokens*)
   14.24 -  val empty = Inttab.empty;
   14.25 -  val extend = I;
   14.26 -  fun merge _ = Inttab.merge (K true);
   14.27 -);
   14.28 -
   14.29 -fun inherit_env context =
   14.30 -  ML_Context.inherit_env context #>
   14.31 -  Extra_Env.put (Extra_Env.get context);
   14.32 -
   14.33 -fun register_tokens toks context =
   14.34 -  let
   14.35 -    val regs = map (fn tok => (serial (), tok)) toks;
   14.36 -    val context' = context
   14.37 -      |> Extra_Env.map (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs);
   14.38 -  in (regs, context') end;
   14.39 -
   14.40 -fun position_of ctxt
   14.41 -    ({file, startLine = line, startPosition = i, endPosition = j, ...}: PolyML.location) =
   14.42 -  (case pairself (Inttab.lookup (Extra_Env.get (Context.Proof ctxt))) (i, j) of
   14.43 -    (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
   14.44 -  | (SOME pos, NONE) => pos
   14.45 -  | _ => Position.line_file line file);
   14.46 -
   14.47 -
   14.48 -(* parse trees *)
   14.49 -
   14.50 -fun report_parse_tree context depth space =
   14.51 -  let
   14.52 -    val pos_of = position_of (Context.proof_of context);
   14.53 -    fun report loc (PolyML.PTtype types) =
   14.54 -          PolyML.NameSpace.displayTypeExpression (types, depth, space)
   14.55 -          |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
   14.56 -          |> Position.report_text Markup.ML_typing (pos_of loc)
   14.57 -      | report loc (PolyML.PTdeclaredAt decl) =
   14.58 -          Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) ""
   14.59 -          |> Position.report_text Markup.ML_ref (pos_of loc)
   14.60 -      | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
   14.61 -      | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
   14.62 -      | report _ _ = ()
   14.63 -    and report_tree (loc, props) = List.app (report loc) props;
   14.64 -  in report_tree end;
   14.65 -
   14.66 -
   14.67 -(* eval ML source tokens *)
   14.68 -
   14.69 -fun use_text ({name_space = space, print, error, ...}: use_context) verbose pos toks =
   14.70 -  let
   14.71 -    (* input *)
   14.72 -
   14.73 -    val input = Context.>>> (register_tokens toks);
   14.74 -    val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input);
   14.75 -
   14.76 -    val current_line = ref (the_default 1 (Position.line_of pos));
   14.77 -
   14.78 -    fun get_index () =
   14.79 -      the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer));
   14.80 -
   14.81 -    fun get () =
   14.82 -      (case ! input_buffer of
   14.83 -        [] => NONE
   14.84 -      | (_, []) :: rest => (input_buffer := rest; get ())
   14.85 -      | (i, c :: cs) :: rest =>
   14.86 -          (input_buffer := (i, cs) :: rest;
   14.87 -           if c = #"\n" then current_line := ! current_line + 1 else ();
   14.88 -           SOME c));
   14.89 -
   14.90 -
   14.91 -    (* output *)
   14.92 -
   14.93 -    val output_buffer = ref Buffer.empty;
   14.94 -    fun output () = Buffer.content (! output_buffer);
   14.95 -    fun put s = change output_buffer (Buffer.add s);
   14.96 -
   14.97 -    fun put_message {message, hard, location, context = _} =
   14.98 -     (put (if hard then "Error: " else "Warning: ");
   14.99 -      put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
  14.100 -      put (Position.str_of
  14.101 -        (position_of (Context.proof_of (the (Context.thread_data ()))) location) ^ "\n"));
  14.102 -
  14.103 -
  14.104 -    (* results *)
  14.105 -
  14.106 -    val depth = get_print_depth ();
  14.107 -
  14.108 -    fun apply_result {fixes, types, signatures, structures, functors, values} =
  14.109 -      let
  14.110 -        fun display disp x =
  14.111 -          if depth > 0 then
  14.112 -            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
  14.113 -          else ();
  14.114 -
  14.115 -        fun apply_fix (a, b) =
  14.116 -          (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
  14.117 -        fun apply_type (a, b) =
  14.118 -          (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b));
  14.119 -        fun apply_sig (a, b) =
  14.120 -          (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
  14.121 -        fun apply_struct (a, b) =
  14.122 -          (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));
  14.123 -        fun apply_funct (a, b) =
  14.124 -          (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));
  14.125 -        fun apply_val (a, b) =
  14.126 -          (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));
  14.127 -      in
  14.128 -        List.app apply_fix fixes;
  14.129 -        List.app apply_type types;
  14.130 -        List.app apply_sig signatures;
  14.131 -        List.app apply_struct structures;
  14.132 -        List.app apply_funct functors;
  14.133 -        List.app apply_val values
  14.134 -      end;
  14.135 -
  14.136 -    fun result_fun (phase1, phase2) () =
  14.137 -     (case phase1 of NONE => ()
  14.138 -      | SOME parse_tree => report_parse_tree (the (Context.thread_data ())) depth space parse_tree;
  14.139 -      case phase2 of NONE => error "Static Errors"
  14.140 -      | SOME code => apply_result (Toplevel.program code));
  14.141 -
  14.142 -
  14.143 -    (* compiler invocation *)
  14.144 -
  14.145 -    val parameters =
  14.146 -     [PolyML.Compiler.CPOutStream put,
  14.147 -      PolyML.Compiler.CPNameSpace space,
  14.148 -      PolyML.Compiler.CPErrorMessageProc put_message,
  14.149 -      PolyML.Compiler.CPLineNo (fn () => ! current_line),
  14.150 -      PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
  14.151 -      PolyML.Compiler.CPLineOffset get_index,
  14.152 -      PolyML.Compiler.CPCompilerResultFun result_fun];
  14.153 -    val _ =
  14.154 -      (while not (List.null (! input_buffer)) do
  14.155 -        PolyML.compiler (get, parameters) ())
  14.156 -      handle exn =>
  14.157 -       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
  14.158 -        error (output ()); raise exn);
  14.159 -  in if verbose then print (output ()) else () end;
  14.160 -
  14.161 -val eval = use_text ML_Context.local_context;
  14.162 -
  14.163 -
  14.164 -(* ML test command *)
  14.165 -
  14.166 -fun ML_test (txt, pos) =
  14.167 -  let
  14.168 -    val _ = Position.report Markup.ML_source pos;
  14.169 -    val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
  14.170 -    val ((env, body), env_ctxt) = ML_Context.eval_antiquotes (ants, pos) (Context.thread_data ());
  14.171 -
  14.172 -    val _ = Context.setmp_thread_data env_ctxt
  14.173 -        (fn () => (eval false Position.none env; Context.thread_data ())) ()
  14.174 -      |> (fn NONE => () | SOME context' => Context.>> (inherit_env context'));
  14.175 -    val _ = eval true pos body;
  14.176 -    val _ = eval false Position.none (ML_Lex.tokenize "structure Isabelle = struct end");
  14.177 -  in () end;
  14.178 -
  14.179 -
  14.180 -local structure P = OuterParse and K = OuterKeyword in
  14.181 -
  14.182 -fun propagate_env (context as Context.Proof lthy) =
  14.183 -      Context.Proof (LocalTheory.map_contexts (inherit_env context) lthy)
  14.184 -  | propagate_env context = context;
  14.185 -
  14.186 -val _ =
  14.187 -  OuterSyntax.command "ML_test" "advanced ML compiler test" (K.tag_ml K.thy_decl)
  14.188 -    (P.ML_source >> (fn src =>
  14.189 -      Toplevel.generic_theory (ML_Context.exec (fn () => ML_test src) #> propagate_env)));
  14.190 -
  14.191 -end;
  14.192 -
  14.193 -end;
  14.194 -
    15.1 --- a/src/Pure/ROOT.ML	Tue Jun 02 14:00:24 2009 +0200
    15.2 +++ b/src/Pure/ROOT.ML	Tue Jun 02 14:38:10 2009 +0200
    15.3 @@ -46,7 +46,6 @@
    15.4  use "Syntax/syntax.ML";
    15.5  
    15.6  use "type_infer.ML";
    15.7 -use "ML/ml_syntax.ML";
    15.8  
    15.9  (*core of tactical proof system*)
   15.10  use "net.ML";
   15.11 @@ -98,6 +97,5 @@
   15.12  (*configuration for Proof General*)
   15.13  cd "ProofGeneral"; use "ROOT.ML"; cd "..";
   15.14  
   15.15 -if ml_system = "polyml-experimental" then use "ML/ml_test.ML" else ();
   15.16  use "pure_setup.ML";
   15.17  
    16.1 --- a/src/Tools/Compute_Oracle/am_compiler.ML	Tue Jun 02 14:00:24 2009 +0200
    16.2 +++ b/src/Tools/Compute_Oracle/am_compiler.ML	Tue Jun 02 14:38:10 2009 +0200
    16.3 @@ -185,7 +185,7 @@
    16.4  
    16.5      in
    16.6  	compiled_rewriter := NONE;	
    16.7 -	use_text ML_Context.local_context (1, "") false (!buffer);
    16.8 +	use_text ML_Env.local_context (1, "") false (!buffer);
    16.9  	case !compiled_rewriter of 
   16.10  	    NONE => raise (Compile "cannot communicate with compiled function")
   16.11  	  | SOME r => (compiled_rewriter := NONE; r)
    17.1 --- a/src/Tools/Compute_Oracle/am_sml.ML	Tue Jun 02 14:00:24 2009 +0200
    17.2 +++ b/src/Tools/Compute_Oracle/am_sml.ML	Tue Jun 02 14:38:10 2009 +0200
    17.3 @@ -492,7 +492,7 @@
    17.4  
    17.5  fun writeTextFile name s = File.write (Path.explode name) s
    17.6  
    17.7 -fun use_source src = use_text ML_Context.local_context (1, "") false src
    17.8 +fun use_source src = use_text ML_Env.local_context (1, "") false src
    17.9      
   17.10  fun compile cache_patterns const_arity eqs = 
   17.11      let
    18.1 --- a/src/Tools/code/code_ml.ML	Tue Jun 02 14:00:24 2009 +0200
    18.2 +++ b/src/Tools/code/code_ml.ML	Tue Jun 02 14:38:10 2009 +0200
    18.3 @@ -1081,7 +1081,7 @@
    18.4  fun isar_seri_sml module_name =
    18.5    Code_Target.parse_args (Scan.succeed ())
    18.6    #> (fn () => serialize_ml target_SML
    18.7 -      (SOME (use_text ML_Context.local_context (1, "generated code") false))
    18.8 +      (SOME (use_text ML_Env.local_context (1, "generated code") false))
    18.9        pr_sml_module pr_sml_stmt module_name);
   18.10  
   18.11  fun isar_seri_ocaml module_name =