1.1 --- a/src/Pure/IsaMakefile	Mon Jun 01 23:28:05 2009 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Mon Jun 01 23:28:06 2009 +0200
     1.3 @@ -65,9 +65,10 @@
     1.4    Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML		\
     1.5    Isar/rule_insts.ML Isar/skip_proof.ML Isar/spec_parse.ML		\
     1.6    Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML		\
     1.7 -  Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_context.ML ML/ml_env.ML	\
     1.8 -  ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_test.ML		\
     1.9 -  ML/ml_thms.ML ML-Systems/install_pp_polyml.ML				\
    1.10 +  Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_compiler.ML		\
    1.11 +  ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML		\
    1.12 +  ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML		\
    1.13 +  ML-Systems/install_pp_polyml.ML					\
    1.14    ML-Systems/install_pp_polyml-experimental.ML				\
    1.15    ML-Systems/use_context.ML Proof/extraction.ML				\
    1.16    Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/ML/ml_compiler.ML	Mon Jun 01 23:28:06 2009 +0200
     2.3 @@ -0,0 +1,23 @@
     2.4 +(*  Title:      Pure/ML/ml_compiler.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Runtime compilation -- generic version.
     2.8 +*)
     2.9 +
    2.10 +signature ML_COMPILER =
    2.11 +sig
    2.12 +  val eval: bool -> Position.T -> ML_Lex.token list -> unit
    2.13 +end
    2.14 +
    2.15 +structure ML_Compiler: ML_COMPILER =
    2.16 +struct
    2.17 +
    2.18 +fun eval verbose pos toks =
    2.19 +  let
    2.20 +    val line = the_default 1 (Position.line_of pos);
    2.21 +    val file = the_default "ML" (Position.file_of pos);
    2.22 +    val text = ML_Lex.flatten toks;
    2.23 +  in Secure.use_text ML_Env.local_context (line, file) verbose text end;
    2.24 +
    2.25 +end;
    2.26 +

     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon Jun 01 23:28:06 2009 +0200
     3.3 @@ -0,0 +1,144 @@
     3.4 +(*  Title:      Pure/ML/ml_compiler_polyml-5.3.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Advanced runtime compilation for Poly/ML 5.3 (SVN 762).
     3.8 +*)
     3.9 +
    3.10 +signature ML_COMPILER =
    3.11 +sig
    3.12 +  val eval: bool -> Position.T -> ML_Lex.token list -> unit
    3.13 +end
    3.14 +
    3.15 +structure ML_Compiler: ML_COMPILER =
    3.16 +struct
    3.17 +
    3.18 +(* original source positions *)
    3.19 +
    3.20 +fun position_of (SOME context) (loc: PolyML.location) =
    3.21 +      (case pairself (ML_Env.token_position context) (#startPosition loc, #endPosition loc) of
    3.22 +        (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
    3.23 +      | (SOME pos, NONE) => pos
    3.24 +      | _ => Position.line_file (#startLine loc) (#file loc))
    3.25 +  | position_of NONE (loc: PolyML.location) = Position.line_file (#startLine loc) (#file loc);
    3.26 +
    3.27 +
    3.28 +(* parse trees *)
    3.29 +
    3.30 +fun report_parse_tree context depth space =
    3.31 +  let
    3.32 +    val pos_of = position_of context;
    3.33 +    fun report loc (PolyML.PTtype types) =
    3.34 +          PolyML.NameSpace.displayTypeExpression (types, depth, space)
    3.35 +          |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    3.36 +          |> Position.report_text Markup.ML_typing (pos_of loc)
    3.37 +      | report loc (PolyML.PTdeclaredAt decl) =
    3.38 +          Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) ""
    3.39 +          |> Position.report_text Markup.ML_ref (pos_of loc)
    3.40 +      | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
    3.41 +      | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
    3.42 +      | report _ _ = ()
    3.43 +    and report_tree (loc, props) = List.app (report loc) props;
    3.44 +  in report_tree end;
    3.45 +
    3.46 +
    3.47 +(* eval ML source tokens *)
    3.48 +
    3.49 +fun eval verbose pos toks =
    3.50 +  let
    3.51 +    val _ = Secure.secure_mltext ();
    3.52 +    val {name_space = space, print, error = err, ...} = ML_Env.local_context;
    3.53 +
    3.54 +
    3.55 +    (* input *)
    3.56 +
    3.57 +    val input =
    3.58 +      if is_none (Context.thread_data ()) then map (pair 0) toks
    3.59 +      else Context.>>> (ML_Env.register_tokens toks);
    3.60 +    val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input);
    3.61 +
    3.62 +    val current_line = ref (the_default 1 (Position.line_of pos));
    3.63 +
    3.64 +    fun get_index () =
    3.65 +      the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer));
    3.66 +
    3.67 +    fun get () =
    3.68 +      (case ! input_buffer of
    3.69 +        [] => NONE
    3.70 +      | (_, []) :: rest => (input_buffer := rest; get ())
    3.71 +      | (i, c :: cs) :: rest =>
    3.72 +          (input_buffer := (i, cs) :: rest;
    3.73 +           if c = #"\n" then current_line := ! current_line + 1 else ();
    3.74 +           SOME c));
    3.75 +
    3.76 +
    3.77 +    (* output *)
    3.78 +
    3.79 +    val output_buffer = ref Buffer.empty;
    3.80 +    fun output () = Buffer.content (! output_buffer);
    3.81 +    fun put s = change output_buffer (Buffer.add s);
    3.82 +
    3.83 +    fun put_message {message, hard, location, context = _} =
    3.84 +     (put (if hard then "Error: " else "Warning: ");
    3.85 +      put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
    3.86 +      put (Position.str_of (position_of (Context.thread_data ()) location) ^ "\n"));
    3.87 +
    3.88 +
    3.89 +    (* results *)
    3.90 +
    3.91 +    val depth = get_print_depth ();
    3.92 +
    3.93 +    fun apply_result {fixes, types, signatures, structures, functors, values} =
    3.94 +      let
    3.95 +        fun display disp x =
    3.96 +          if depth > 0 then
    3.97 +            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
    3.98 +          else ();
    3.99 +
   3.100 +        fun apply_fix (a, b) =
   3.101 +          (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
   3.102 +        fun apply_type (a, b) =
   3.103 +          (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b));
   3.104 +        fun apply_sig (a, b) =
   3.105 +          (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
   3.106 +        fun apply_struct (a, b) =
   3.107 +          (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));
   3.108 +        fun apply_funct (a, b) =
   3.109 +          (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));
   3.110 +        fun apply_val (a, b) =
   3.111 +          (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));
   3.112 +      in
   3.113 +        List.app apply_fix fixes;
   3.114 +        List.app apply_type types;
   3.115 +        List.app apply_sig signatures;
   3.116 +        List.app apply_struct structures;
   3.117 +        List.app apply_funct functors;
   3.118 +        List.app apply_val values
   3.119 +      end;
   3.120 +
   3.121 +    fun result_fun (phase1, phase2) () =
   3.122 +     (case phase1 of NONE => ()
   3.123 +      | SOME parse_tree => report_parse_tree (Context.thread_data ()) depth space parse_tree;
   3.124 +      case phase2 of NONE => err "Static Errors"
   3.125 +      | SOME code => apply_result (code ()));  (* FIXME Toplevel.program *)
   3.126 +
   3.127 +
   3.128 +    (* compiler invocation *)
   3.129 +
   3.130 +    val parameters =
   3.131 +     [PolyML.Compiler.CPOutStream put,
   3.132 +      PolyML.Compiler.CPNameSpace space,
   3.133 +      PolyML.Compiler.CPErrorMessageProc put_message,
   3.134 +      PolyML.Compiler.CPLineNo (fn () => ! current_line),
   3.135 +      PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
   3.136 +      PolyML.Compiler.CPLineOffset get_index,
   3.137 +      PolyML.Compiler.CPCompilerResultFun result_fun];
   3.138 +    val _ =
   3.139 +      (while not (List.null (! input_buffer)) do
   3.140 +        PolyML.compiler (get, parameters) ())
   3.141 +      handle exn =>
   3.142 +       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
   3.143 +        err (output ()); raise exn);
   3.144 +  in if verbose then print (output ()) else () end;
   3.145 +
   3.146 +end;
   3.147 +

     4.1 --- a/src/Pure/ML/ml_test.ML	Mon Jun 01 23:28:05 2009 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,172 +0,0 @@
     4.4 -(*  Title:      Pure/ML/ml_test.ML
     4.5 -    Author:     Makarius
     4.6 -
     4.7 -Test of advanced ML compiler invocation in Poly/ML 5.3 (SVN 762).
     4.8 -*)
     4.9 -
    4.10 -signature ML_TEST =
    4.11 -sig
    4.12 -  val position_of: Proof.context -> PolyML.location -> Position.T
    4.13 -  val eval: bool -> Position.T -> ML_Lex.token list -> unit
    4.14 -end
    4.15 -
    4.16 -structure ML_Test: ML_TEST =
    4.17 -struct
    4.18 -
    4.19 -(* extra ML environment *)
    4.20 -
    4.21 -fun position_of ctxt
    4.22 -    ({file, startLine = line, startPosition = i, endPosition = j, ...}: PolyML.location) =
    4.23 -  (case pairself (ML_Env.token_position ctxt) (i, j) of
    4.24 -    (SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
    4.25 -  | (SOME pos, NONE) => pos
    4.26 -  | _ => Position.line_file line file);
    4.27 -
    4.28 -
    4.29 -(* parse trees *)
    4.30 -
    4.31 -fun report_parse_tree context depth space =
    4.32 -  let
    4.33 -    val pos_of = position_of (Context.proof_of context);
    4.34 -    fun report loc (PolyML.PTtype types) =
    4.35 -          PolyML.NameSpace.displayTypeExpression (types, depth, space)
    4.36 -          |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    4.37 -          |> Position.report_text Markup.ML_typing (pos_of loc)
    4.38 -      | report loc (PolyML.PTdeclaredAt decl) =
    4.39 -          Markup.markup (Markup.properties (Position.properties_of (pos_of decl)) Markup.ML_def) ""
    4.40 -          |> Position.report_text Markup.ML_ref (pos_of loc)
    4.41 -      | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
    4.42 -      | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
    4.43 -      | report _ _ = ()
    4.44 -    and report_tree (loc, props) = List.app (report loc) props;
    4.45 -  in report_tree end;
    4.46 -
    4.47 -
    4.48 -(* eval ML source tokens *)
    4.49 -
    4.50 -fun use_text ({name_space = space, print, error, ...}: use_context) verbose pos toks =
    4.51 -  let
    4.52 -    (* input *)
    4.53 -
    4.54 -    val input = Context.>>> (ML_Env.register_tokens toks);
    4.55 -    val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input);
    4.56 -
    4.57 -    val current_line = ref (the_default 1 (Position.line_of pos));
    4.58 -
    4.59 -    fun get_index () =
    4.60 -      the_default 0 (get_first (fn (_, []) => NONE | (i, _) => SOME i) (! input_buffer));
    4.61 -
    4.62 -    fun get () =
    4.63 -      (case ! input_buffer of
    4.64 -        [] => NONE
    4.65 -      | (_, []) :: rest => (input_buffer := rest; get ())
    4.66 -      | (i, c :: cs) :: rest =>
    4.67 -          (input_buffer := (i, cs) :: rest;
    4.68 -           if c = #"\n" then current_line := ! current_line + 1 else ();
    4.69 -           SOME c));
    4.70 -
    4.71 -
    4.72 -    (* output *)
    4.73 -
    4.74 -    val output_buffer = ref Buffer.empty;
    4.75 -    fun output () = Buffer.content (! output_buffer);
    4.76 -    fun put s = change output_buffer (Buffer.add s);
    4.77 -
    4.78 -    fun put_message {message, hard, location, context = _} =
    4.79 -     (put (if hard then "Error: " else "Warning: ");
    4.80 -      put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
    4.81 -      put (Position.str_of
    4.82 -        (position_of (Context.proof_of (the (Context.thread_data ()))) location) ^ "\n"));
    4.83 -
    4.84 -
    4.85 -    (* results *)
    4.86 -
    4.87 -    val depth = get_print_depth ();
    4.88 -
    4.89 -    fun apply_result {fixes, types, signatures, structures, functors, values} =
    4.90 -      let
    4.91 -        fun display disp x =
    4.92 -          if depth > 0 then
    4.93 -            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
    4.94 -          else ();
    4.95 -
    4.96 -        fun apply_fix (a, b) =
    4.97 -          (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
    4.98 -        fun apply_type (a, b) =
    4.99 -          (display PolyML.NameSpace.displayType (b, depth, space); #enterType space (a, b));
   4.100 -        fun apply_sig (a, b) =
   4.101 -          (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
   4.102 -        fun apply_struct (a, b) =
   4.103 -          (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));
   4.104 -        fun apply_funct (a, b) =
   4.105 -          (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));
   4.106 -        fun apply_val (a, b) =
   4.107 -          (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));
   4.108 -      in
   4.109 -        List.app apply_fix fixes;
   4.110 -        List.app apply_type types;
   4.111 -        List.app apply_sig signatures;
   4.112 -        List.app apply_struct structures;
   4.113 -        List.app apply_funct functors;
   4.114 -        List.app apply_val values
   4.115 -      end;
   4.116 -
   4.117 -    fun result_fun (phase1, phase2) () =
   4.118 -     (case phase1 of NONE => ()
   4.119 -      | SOME parse_tree => report_parse_tree (the (Context.thread_data ())) depth space parse_tree;
   4.120 -      case phase2 of NONE => error "Static Errors"
   4.121 -      | SOME code => apply_result (Toplevel.program code));
   4.122 -
   4.123 -
   4.124 -    (* compiler invocation *)
   4.125 -
   4.126 -    val parameters =
   4.127 -     [PolyML.Compiler.CPOutStream put,
   4.128 -      PolyML.Compiler.CPNameSpace space,
   4.129 -      PolyML.Compiler.CPErrorMessageProc put_message,
   4.130 -      PolyML.Compiler.CPLineNo (fn () => ! current_line),
   4.131 -      PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
   4.132 -      PolyML.Compiler.CPLineOffset get_index,
   4.133 -      PolyML.Compiler.CPCompilerResultFun result_fun];
   4.134 -    val _ =
   4.135 -      (while not (List.null (! input_buffer)) do
   4.136 -        PolyML.compiler (get, parameters) ())
   4.137 -      handle exn =>
   4.138 -       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
   4.139 -        error (output ()); raise exn);
   4.140 -  in if verbose then print (output ()) else () end;
   4.141 -
   4.142 -val eval = use_text ML_Env.local_context;
   4.143 -
   4.144 -
   4.145 -(* ML test command *)
   4.146 -
   4.147 -fun ML_test (txt, pos) =
   4.148 -  let
   4.149 -    val _ = Position.report Markup.ML_source pos;
   4.150 -    val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
   4.151 -    val ((env, body), env_ctxt) = ML_Context.eval_antiquotes (ants, pos) (Context.thread_data ());
   4.152 -
   4.153 -    val _ = Context.setmp_thread_data env_ctxt
   4.154 -        (fn () => (eval false Position.none env; Context.thread_data ())) ()
   4.155 -      |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
   4.156 -    val _ = eval true pos body;
   4.157 -    val _ = eval false Position.none (ML_Lex.tokenize "structure Isabelle = struct end");
   4.158 -  in () end;
   4.159 -
   4.160 -
   4.161 -local structure P = OuterParse and K = OuterKeyword in
   4.162 -
   4.163 -fun propagate_env (context as Context.Proof lthy) =
   4.164 -      Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
   4.165 -  | propagate_env context = context;
   4.166 -
   4.167 -val _ =
   4.168 -  OuterSyntax.command "ML_test" "advanced ML compiler test" (K.tag_ml K.thy_decl)
   4.169 -    (P.ML_source >> (fn src =>
   4.170 -      Toplevel.generic_theory (ML_Context.exec (fn () => ML_test src) #> propagate_env)));
   4.171 -
   4.172 -end;
   4.173 -
   4.174 -end;
   4.175 -

     5.1 --- a/src/Pure/ROOT.ML	Mon Jun 01 23:28:05 2009 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Mon Jun 01 23:28:06 2009 +0200
     5.3 @@ -56,6 +56,10 @@
     5.4  use "General/secure.ML";
     5.5  use "General/file.ML";
     5.6  
     5.7 +if ml_system = "polyml-experimental"
     5.8 +then use "ML/ml_compiler_polyml-5.3.ML"
     5.9 +else use "ML/ml_compiler.ML";
    5.10 +
    5.11  (*core of tactical proof system*)
    5.12  use "net.ML";
    5.13  use "item_net.ML";
    5.14 @@ -106,6 +110,5 @@
    5.15  (*configuration for Proof General*)
    5.16  cd "ProofGeneral"; use "ROOT.ML"; cd "..";
    5.17  
    5.18 -if ml_system = "polyml-experimental" then use "ML/ml_test.ML" else ();
    5.19  use "pure_setup.ML";
    5.20