--- a/Admin/isatest/isatest-stats Tue Mar 24 14:08:13 2009 +0100
+++ b/Admin/isatest/isatest-stats Tue Mar 24 14:09:24 2009 +0100
@@ -1,13 +1,12 @@
#!/usr/bin/env bash
#
-# $Id$
# Author: Makarius
#
# DESCRIPTION: Standard statistics.
THIS=$(cd "$(dirname "$0")"; pwd -P)
-PLATFORMS="at-poly at-sml-dev at64-poly at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp"
+PLATFORMS="at-poly at64-poly at-poly-5.1-para-e at64-poly-5.1-para at-mac-poly-5.1-para afp at-sml-dev"
ISABELLE_SESSIONS="\
HOL-Plain \
--- a/src/Pure/General/antiquote.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/General/antiquote.ML Tue Mar 24 14:09:24 2009 +0100
@@ -8,7 +8,7 @@
sig
datatype 'a antiquote =
Text of 'a |
- Antiq of Symbol_Pos.T list * Position.T |
+ Antiq of Symbol_Pos.T list * Position.range |
Open of Position.T |
Close of Position.T
val is_text: 'a antiquote -> bool
@@ -26,7 +26,7 @@
datatype 'a antiquote =
Text of 'a |
- Antiq of Symbol_Pos.T list * Position.T |
+ Antiq of Symbol_Pos.T list * Position.range |
Open of Position.T |
Close of Position.T;
@@ -39,7 +39,7 @@
val report_antiq = Position.report Markup.antiq;
fun report report_text (Text x) = report_text x
- | report _ (Antiq (_, pos)) = report_antiq pos
+ | report _ (Antiq (_, (pos, _))) = report_antiq pos
| report _ (Open pos) = report_antiq pos
| report _ (Close pos) = report_antiq pos;
@@ -79,7 +79,7 @@
Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |--
Symbol_Pos.!!! "missing closing brace of antiquotation"
(Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos)))
- >> (fn (pos1, (body, pos2)) => (flat body, Position.encode_range (pos1, pos2)));
+ >> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2));
val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>";
val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>";
--- a/src/Pure/General/output.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/General/output.ML Tue Mar 24 14:09:24 2009 +0100
@@ -47,7 +47,6 @@
val debugging: bool ref
val no_warnings: ('a -> 'b) -> 'a -> 'b
val debug: (unit -> string) -> unit
- val ml_output: (string -> unit) * (string -> 'a)
val accumulated_time: unit -> unit
end;
@@ -101,7 +100,7 @@
val error_fn = ref (std_output o suffix "\n" o prefix_lines "*** ");
val debug_fn = ref (std_output o suffix "\n" o prefix_lines "::: ");
val prompt_fn = ref std_output;
-val status_fn = ref (fn s => ! writeln_fn s);
+val status_fn = ref (fn _: string => ());
fun writeln s = ! writeln_fn (output s);
fun priority s = ! priority_fn (output s);
@@ -120,8 +119,6 @@
val debugging = ref false;
fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
-val ml_output = (writeln, error);
-
(** timing **)
--- a/src/Pure/General/position.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/General/position.ML Tue Mar 24 14:09:24 2009 +0100
@@ -24,6 +24,7 @@
val of_properties: Properties.T -> T
val properties_of: T -> Properties.T
val default_properties: T -> Properties.T -> Properties.T
+ val report_text: Markup.T -> T -> string -> unit
val report: Markup.T -> T -> unit
val str_of: T -> string
type range = T * T
@@ -121,9 +122,11 @@
if exists (member (op =) Markup.position_properties o #1) props then props
else properties_of default @ props;
-fun report markup (pos as Pos (count, _)) =
+fun report_text markup (pos as Pos (count, _)) txt =
if invalid_count count then ()
- else Output.status (Markup.markup (Markup.properties (properties_of pos) markup) "");
+ else Output.status (Markup.markup (Markup.properties (properties_of pos) markup) txt);
+
+fun report markup pos = report_text markup pos "";
(* str_of *)
--- a/src/Pure/General/secure.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/General/secure.ML Tue Mar 24 14:09:24 2009 +0100
@@ -9,11 +9,8 @@
val set_secure: unit -> unit
val is_secure: unit -> bool
val deny_secure: string -> unit
- val use_text: ML_NameSpace.nameSpace -> int * string ->
- (string -> unit) * (string -> 'a) -> bool -> string -> unit
- val use_file: ML_NameSpace.nameSpace ->
- (string -> unit) * (string -> 'a) -> bool -> string -> unit
- val use: string -> unit
+ val use_text: use_context -> int * string -> bool -> string -> unit
+ val use_file: use_context -> bool -> string -> unit
val toplevel_pp: string list -> string -> unit
val commit: unit -> unit
val system_out: string -> string * int
@@ -40,23 +37,17 @@
fun secure_mltext () = deny_secure "Cannot evaluate ML source in secure mode";
-fun raw_use_text ns = use_text ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
-fun raw_use_file ns = use_file ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
-fun raw_toplevel_pp x =
- toplevel_pp ML_Parse.fix_ints (Position.str_of oo Position.line_file) Output.ml_output x;
+val raw_use_text = use_text;
+val raw_use_file = use_file;
+val raw_toplevel_pp = toplevel_pp;
-fun use_text ns pos pr verbose txt =
- (secure_mltext (); raw_use_text ns pos pr verbose txt);
+fun use_text context pos verbose txt = (secure_mltext (); raw_use_text context pos verbose txt);
+fun use_file context verbose name = (secure_mltext (); raw_use_file context verbose name);
-fun use_file ns pr verbose name =
- (secure_mltext (); raw_use_file ns pr verbose name);
-
-fun use name = use_file ML_NameSpace.global Output.ml_output true name;
-
-fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp path pp);
+fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
(*commit is dynamically bound!*)
-fun commit () = raw_use_text ML_NameSpace.global (0, "") Output.ml_output false "commit();";
+fun commit () = raw_use_text ML_Parse.global_context (0, "") false "commit();";
(* shell commands *)
@@ -77,7 +68,8 @@
(*override previous toplevel bindings!*)
val use_text = Secure.use_text;
val use_file = Secure.use_file;
-fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
+fun use s = Secure.use_file ML_Parse.global_context true s
+ handle ERROR msg => (writeln msg; raise Fail "ML error");
val toplevel_pp = Secure.toplevel_pp;
val system_out = Secure.system_out;
val system = Secure.system;
--- a/src/Pure/IsaMakefile Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/IsaMakefile Tue Mar 24 14:09:24 2009 +0100
@@ -70,7 +70,8 @@
Isar/toplevel.ML Isar/value_parse.ML ML/ml_antiquote.ML \
ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML \
ML/ml_test.ML ML/ml_thms.ML ML-Systems/install_pp_polyml.ML \
- ML-Systems/install_pp_polyml-experimental.ML Proof/extraction.ML \
+ ML-Systems/install_pp_polyml-experimental.ML \
+ ML-Systems/use_context.ML Proof/extraction.ML \
Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML \
ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \
--- a/src/Pure/Isar/outer_keyword.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/Isar/outer_keyword.ML Tue Mar 24 14:09:24 2009 +0100
@@ -150,23 +150,25 @@
Pretty.mark (Markup.command_decl name (kind_of kind))
(Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));
+fun status_writeln s = (Output.status s; writeln s);
+
fun report () =
let val (keywords, commands) = CRITICAL (fn () =>
(dest_keywords (), sort_wrt #1 (Symtab.dest (get_commands ()))))
in map report_keyword keywords @ map report_command commands end
- |> Pretty.chunks |> Pretty.string_of |> Output.status;
+ |> Pretty.chunks |> Pretty.string_of |> status_writeln;
(* augment tables *)
fun keyword name =
(change_lexicons (apfst (Scan.extend_lexicon (Symbol.explode name)));
- Output.status (Pretty.string_of (report_keyword name)));
+ status_writeln (Pretty.string_of (report_keyword name)));
fun command name kind =
(change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));
change_commands (Symtab.update (name, kind));
- Output.status (Pretty.string_of (report_command (name, kind))));
+ status_writeln (Pretty.string_of (report_command (name, kind))));
(* command categories *)
--- a/src/Pure/ML-Systems/ml_name_space.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML-Systems/ml_name_space.ML Tue Mar 24 14:09:24 2009 +0100
@@ -4,7 +4,7 @@
ML name space -- dummy version of Poly/ML 5.2 facility.
*)
-structure ML_NameSpace =
+structure ML_Name_Space =
struct
type valueVal = unit;
@@ -14,7 +14,7 @@
type signatureVal = unit;
type functorVal = unit;
-type nameSpace =
+type T =
{lookupVal: string -> valueVal option,
lookupType: string -> typeVal option,
lookupFix: string -> fixityVal option,
@@ -34,7 +34,7 @@
allSig: unit -> (string * signatureVal) list,
allFunct: unit -> (string * functorVal) list};
-val global: nameSpace =
+val global: T =
{lookupVal = fn _ => NONE,
lookupType = fn _ => NONE,
lookupFix = fn _ => NONE,
--- a/src/Pure/ML-Systems/mosml.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML-Systems/mosml.ML Tue Mar 24 14:09:24 2009 +0100
@@ -46,6 +46,7 @@
use "ML-Systems/time_limit.ML";
use "ML-Systems/ml_name_space.ML";
use "ML-Systems/ml_pretty.ML";
+use "ML-Systems/use_context.ML";
(*low-level pointer equality*)
@@ -120,7 +121,7 @@
end;
(*dummy implementation*)
-fun toplevel_pp _ _ _ _ _ = ();
+fun toplevel_pp _ _ _ = ();
(*dummy implementation*)
fun ml_prompts p1 p2 = ();
@@ -185,18 +186,18 @@
(* ML command execution *)
(*Can one redirect 'use' directly to an instream?*)
-fun use_text (tune: string -> string) _ _ _ _ _ txt =
+fun use_text ({tune_source, ...}: use_context) _ _ txt =
let
val tmp_name = FileSys.tmpName ();
val tmp_file = TextIO.openOut tmp_name;
in
- TextIO.output (tmp_file, tune txt);
+ TextIO.output (tmp_file, tune_source txt);
TextIO.closeOut tmp_file;
use tmp_name;
FileSys.remove tmp_name
end;
-fun use_file _ _ _ _ _ name = use name;
+fun use_file _ _ name = use name;
--- a/src/Pure/ML-Systems/polyml-4.1.3.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.1.3.ML Tue Mar 24 14:09:24 2009 +0100
@@ -6,6 +6,7 @@
use "ML-Systems/polyml_old_basis.ML";
use "ML-Systems/universal.ML";
use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/ml_name_space.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler4.ML";
use "ML-Systems/polyml_pp.ML";
--- a/src/Pure/ML-Systems/polyml-4.1.4.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.1.4.ML Tue Mar 24 14:09:24 2009 +0100
@@ -6,6 +6,7 @@
use "ML-Systems/polyml_old_basis.ML";
use "ML-Systems/universal.ML";
use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/ml_name_space.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler4.ML";
use "ML-Systems/polyml_pp.ML";
--- a/src/Pure/ML-Systems/polyml-4.2.0.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-4.2.0.ML Tue Mar 24 14:09:24 2009 +0100
@@ -5,6 +5,7 @@
use "ML-Systems/universal.ML";
use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/ml_name_space.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler4.ML";
use "ML-Systems/polyml_pp.ML";
--- a/src/Pure/ML-Systems/polyml-5.0.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.0.ML Tue Mar 24 14:09:24 2009 +0100
@@ -5,6 +5,7 @@
use "ML-Systems/universal.ML";
use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/ml_name_space.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler5.ML";
use "ML-Systems/polyml_pp.ML";
--- a/src/Pure/ML-Systems/polyml-5.1.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-5.1.ML Tue Mar 24 14:09:24 2009 +0100
@@ -4,6 +4,7 @@
*)
use "ML-Systems/thread_dummy.ML";
+use "ML-Systems/ml_name_space.ML";
use "ML-Systems/polyml_common.ML";
use "ML-Systems/polyml_old_compiler5.ML";
use "ML-Systems/polyml_pp.ML";
--- a/src/Pure/ML-Systems/polyml-experimental.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-experimental.ML Tue Mar 24 14:09:24 2009 +0100
@@ -4,6 +4,14 @@
*)
open Thread;
+
+structure ML_Name_Space =
+struct
+ open PolyML.NameSpace;
+ type T = PolyML.NameSpace.nameSpace;
+ val global = PolyML.globalNameSpace;
+end;
+
use "ML-Systems/polyml_common.ML";
use "ML-Systems/multithreading_polyml.ML";
@@ -14,12 +22,6 @@
(* runtime compilation *)
-structure ML_NameSpace =
-struct
- open PolyML.NameSpace;
- val global = PolyML.globalNameSpace;
-end;
-
local
fun drop_newline s =
@@ -28,11 +30,11 @@
in
-fun use_text (tune: string -> string) str_of_pos
- name_space (start_line, name) (print, err) verbose txt =
+fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
+ (start_line, name) verbose txt =
let
val current_line = ref start_line;
- val in_buffer = ref (String.explode (tune txt));
+ val in_buffer = ref (String.explode (tune_source txt));
val out_buffer = ref ([]: string list);
fun output () = drop_newline (implode (rev (! out_buffer)));
@@ -42,10 +44,11 @@
| c :: cs =>
(in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
fun put s = out_buffer := s :: ! out_buffer;
- fun put_message {message, hard, location = {startLine = line, ...}, context} =
+ fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
(put (if hard then "Error: " else "Warning: ");
- PolyML.prettyPrint (put, 76) message;
- put (str_of_pos line name ^ "\n"));
+ PolyML.prettyPrint (put, 76) msg1;
+ (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
+ put ("At" ^ str_of_pos line name ^ "\n"));
val parameters =
[PolyML.Compiler.CPOutStream put,
@@ -58,30 +61,50 @@
PolyML.compiler (get, parameters) ())
handle exn =>
(put ("Exception- " ^ General.exnMessage exn ^ " raised");
- err (output ()); raise exn);
+ error (output ()); raise exn);
in if verbose then print (output ()) else () end;
-fun use_file tune str_of_pos name_space output verbose name =
+fun use_file context verbose name =
let
val instream = TextIO.openIn name;
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text tune str_of_pos name_space (1, name) output verbose txt end;
+ in use_text context (1, name) verbose txt end;
end;
(* toplevel pretty printing *)
-fun pretty_ml (PrettyBlock (ind, _, _, prts)) = ML_Pretty.Block (("", ""), map pretty_ml prts, ind)
- | pretty_ml (PrettyString s) = ML_Pretty.String (s, size s)
- | pretty_ml (PrettyBreak (wd, _)) = ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
+val pretty_ml =
+ let
+ fun convert len (PrettyBlock (ind, _, context, prts)) =
+ let
+ fun property name default =
+ (case List.find (fn ContextProperty (a, _) => name = a | _ => false) context of
+ SOME (ContextProperty (_, b)) => b
+ | NONE => default);
+ val bg = property "begin" "";
+ val en = property "end" "";
+ val len' = property "length" len;
+ in ML_Pretty.Block ((bg, en), map (convert len') prts, ind) end
+ | convert len (PrettyString s) =
+ ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
+ | convert _ (PrettyBreak (wd, _)) =
+ ML_Pretty.Break (if wd < 99999 then (false, wd) else (true, 2));
+ in convert "" end;
-fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts)
- | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s
+fun ml_pretty (ML_Pretty.Block ((bg, en), prts, ind)) =
+ let val context =
+ (if bg = "" then [] else [ContextProperty ("begin", bg)]) @
+ (if en = "" then [] else [ContextProperty ("end", en)])
+ in PrettyBlock (ind, false, context, map ml_pretty prts) end
+ | ml_pretty (ML_Pretty.String (s, len)) =
+ if len = size s then PrettyString s
+ else PrettyBlock (0, false, [ContextProperty ("length", Int.toString len)], [PrettyString s])
| ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
| ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0);
-fun toplevel_pp tune str_of_pos output (_: string list) pp =
- use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+fun toplevel_pp context (_: string list) pp =
+ use_text context (1, "pp") false
("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
--- a/src/Pure/ML-Systems/polyml.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Tue Mar 24 14:09:24 2009 +0100
@@ -4,6 +4,14 @@
*)
open Thread;
+
+structure ML_Name_Space =
+struct
+ open PolyML.NameSpace;
+ type T = PolyML.NameSpace.nameSpace;
+ val global = PolyML.globalNameSpace;
+end;
+
use "ML-Systems/polyml_common.ML";
if ml_system = "polyml-5.2"
@@ -17,12 +25,6 @@
(* runtime compilation *)
-structure ML_NameSpace =
-struct
- open PolyML.NameSpace;
- val global = PolyML.globalNameSpace;
-end;
-
local
fun drop_newline s =
@@ -31,11 +33,11 @@
in
-fun use_text (tune: string -> string) str_of_pos
- name_space (start_line, name) (print, err) verbose txt =
+fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
+ (start_line, name) verbose txt =
let
val current_line = ref start_line;
- val in_buffer = ref (String.explode (tune txt));
+ val in_buffer = ref (String.explode (tune_source txt));
val out_buffer = ref ([]: string list);
fun output () = drop_newline (implode (rev (! out_buffer)));
@@ -58,14 +60,14 @@
PolyML.compiler (get, parameters) ())
handle exn =>
(put ("Exception- " ^ General.exnMessage exn ^ " raised");
- err (output ()); raise exn);
+ error (output ()); raise exn);
in if verbose then print (output ()) else () end;
-fun use_file tune str_of_pos name_space output verbose name =
+fun use_file context verbose name =
let
val instream = TextIO.openIn name;
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text tune str_of_pos name_space (1, name) output verbose txt end;
+ in use_text context (1, name) verbose txt end;
end;
--- a/src/Pure/ML-Systems/polyml_common.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML Tue Mar 24 14:09:24 2009 +0100
@@ -9,8 +9,8 @@
use "ML-Systems/multithreading.ML";
use "ML-Systems/time_limit.ML";
use "ML-Systems/system_shell.ML";
-use "ML-Systems/ml_name_space.ML";
use "ML-Systems/ml_pretty.ML";
+use "ML-Systems/use_context.ML";
(** ML system and platform related **)
--- a/src/Pure/ML-Systems/polyml_old_compiler4.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML Tue Mar 24 14:09:24 2009 +0100
@@ -3,9 +3,9 @@
Runtime compilation -- for old PolyML.compiler (version 4.x).
*)
-fun use_text (tune: string -> string) _ _ (line: int, name) (print, err) verbose txt =
+fun use_text ({tune_source, print, error, ...}: use_context) (line: int, name) verbose txt =
let
- val in_buffer = ref (explode (tune txt));
+ val in_buffer = ref (explode (tune_source txt));
val out_buffer = ref ([]: string list);
fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
@@ -21,12 +21,12 @@
| _ => (PolyML.compiler (get, put) (); exec ()));
in
exec () handle exn =>
- (err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
+ (error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
if verbose then print (output ()) else ()
end;
-fun use_file tune str_of_pos name_space output verbose name =
+fun use_file context verbose name =
let
val instream = TextIO.openIn name;
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text tune str_of_pos name_space (1, name) output verbose txt end;
+ in use_text context (1, name) verbose txt end;
--- a/src/Pure/ML-Systems/polyml_old_compiler5.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_old_compiler5.ML Tue Mar 24 14:09:24 2009 +0100
@@ -3,9 +3,9 @@
Runtime compilation -- for old PolyML.compilerEx (version 5.0, 5.1).
*)
-fun use_text (tune: string -> string) _ _ (line, name) (print, err) verbose txt =
+fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
let
- val in_buffer = ref (explode (tune txt));
+ val in_buffer = ref (explode (tune_source txt));
val out_buffer = ref ([]: string list);
fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
@@ -21,12 +21,12 @@
[] => ()
| _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
in
- exec () handle exn => (err (output ()); raise exn);
+ exec () handle exn => (error (output ()); raise exn);
if verbose then print (output ()) else ()
end;
-fun use_file tune str_of_pos name_space output verbose name =
+fun use_file context verbose name =
let
val instream = TextIO.openIn name;
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text tune str_of_pos name_space (1, name) output verbose txt end;
+ in use_text context (1, name) verbose txt end;
--- a/src/Pure/ML-Systems/polyml_pp.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML-Systems/polyml_pp.ML Tue Mar 24 14:09:24 2009 +0100
@@ -14,7 +14,7 @@
| pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
in pprint end;
-fun toplevel_pp tune str_of_pos output (_: string list) pp =
- use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+fun toplevel_pp context (_: string list) pp =
+ use_text context (1, "pp") false
("install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
--- a/src/Pure/ML-Systems/smlnj.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Tue Mar 24 14:09:24 2009 +0100
@@ -14,6 +14,7 @@
use "ML-Systems/system_shell.ML";
use "ML-Systems/ml_name_space.ML";
use "ML-Systems/ml_pretty.ML";
+use "ML-Systems/use_context.ML";
(*low-level pointer equality*)
@@ -100,7 +101,7 @@
(* ML command execution *)
-fun use_text (tune: string -> string) _ _ (line: int, name) (print, err) verbose txt =
+fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
let
val ref out_orig = Control.Print.out;
@@ -111,22 +112,20 @@
in String.substring (str, 0, Int.max (0, size str - 1)) end;
in
Control.Print.out := out;
- Backend.Interact.useStream (TextIO.openString (tune txt)) handle exn =>
+ Backend.Interact.useStream (TextIO.openString (tune_source txt)) handle exn =>
(Control.Print.out := out_orig;
- err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
+ error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
Control.Print.out := out_orig;
if verbose then print (output ()) else ()
end;
-fun use_file tune str_of_pos name_space output verbose name =
+fun use_file context verbose name =
let
val instream = TextIO.openIn name;
val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text tune str_of_pos name_space (1, name) output verbose txt end;
+ in use_text context (1, name) verbose txt end;
-fun forget_structure name =
- use_text (fn x => x) (fn _ => "") () (1, "ML") (TextIO.print, fn s => raise Fail s) false
- ("structure " ^ name ^ " = struct end");
+fun forget_structure _ = ();
(* toplevel pretty printing *)
@@ -143,8 +142,8 @@
| pprint (ML_Pretty.Break (true, _)) = PrettyPrint.newline pps;
in pprint end;
-fun toplevel_pp tune str_of_pos output path pp =
- use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+fun toplevel_pp context path pp =
+ use_text context (1, "pp") false
("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"") path) ^
"] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/use_context.ML Tue Mar 24 14:09:24 2009 +0100
@@ -0,0 +1,13 @@
+(* Title: Pure/ML-Systems/use_context.ML
+ Author: Makarius
+
+Common context for "use" operations (compiler invocation).
+*)
+
+type use_context =
+ {tune_source: string -> string,
+ name_space: ML_Name_Space.T,
+ str_of_pos: int -> string -> string,
+ print: string -> unit,
+ error: string -> unit};
+
--- a/src/Pure/ML/ml_context.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML/ml_context.ML Tue Mar 24 14:09:24 2009 +0100
@@ -20,7 +20,8 @@
val the_local_context: unit -> Proof.context
val exec: (unit -> unit) -> Context.generic -> Context.generic
val inherit_env: Context.generic -> Context.generic -> Context.generic
- val name_space: ML_NameSpace.nameSpace
+ val name_space: ML_Name_Space.T
+ val local_context: use_context
val stored_thms: thm list ref
val ml_store_thm: string * thm -> unit
val ml_store_thms: string * thm list -> unit
@@ -31,13 +32,10 @@
val trace: bool ref
val eval_antiquotes: ML_Lex.token Antiquote.antiquote list * Position.T ->
Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
- val eval_wrapper: (string -> unit) * (string -> 'a) -> bool ->
- Position.T -> Symbol_Pos.text -> unit
val eval: bool -> Position.T -> Symbol_Pos.text -> unit
val eval_file: Path.T -> unit
val eval_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
- val evaluate: Proof.context -> (string -> unit) * (string -> 'b) -> bool ->
- string * (unit -> 'a) option ref -> string -> 'a
+ val evaluate: Proof.context -> bool -> string * (unit -> 'a) option ref -> string -> 'a
val expression: Position.T -> string -> string -> string -> Context.generic -> Context.generic
end
@@ -61,12 +59,12 @@
structure ML_Env = GenericDataFun
(
type T =
- ML_NameSpace.valueVal Symtab.table *
- ML_NameSpace.typeVal Symtab.table *
- ML_NameSpace.fixityVal Symtab.table *
- ML_NameSpace.structureVal Symtab.table *
- ML_NameSpace.signatureVal Symtab.table *
- ML_NameSpace.functorVal Symtab.table;
+ ML_Name_Space.valueVal Symtab.table *
+ ML_Name_Space.typeVal Symtab.table *
+ ML_Name_Space.fixityVal Symtab.table *
+ ML_Name_Space.structureVal Symtab.table *
+ ML_Name_Space.signatureVal Symtab.table *
+ ML_Name_Space.functorVal Symtab.table;
val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
val extend = I;
fun merge _
@@ -82,23 +80,23 @@
val inherit_env = ML_Env.put o ML_Env.get;
-val name_space: ML_NameSpace.nameSpace =
+val name_space: ML_Name_Space.T =
let
fun lookup sel1 sel2 name =
Context.thread_data ()
|> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (ML_Env.get context)) name)
- |> (fn NONE => sel2 ML_NameSpace.global name | some => some);
+ |> (fn NONE => sel2 ML_Name_Space.global name | some => some);
fun all sel1 sel2 () =
Context.thread_data ()
|> (fn NONE => [] | SOME context => Symtab.dest (sel1 (ML_Env.get context)))
- |> append (sel2 ML_NameSpace.global ())
+ |> append (sel2 ML_Name_Space.global ())
|> sort_distinct (string_ord o pairself #1);
fun enter ap1 sel2 entry =
if is_some (Context.thread_data ()) then
Context.>> (ML_Env.map (ap1 (Symtab.update entry)))
- else sel2 ML_NameSpace.global entry;
+ else sel2 ML_Name_Space.global entry;
in
{lookupVal = lookup #1 #lookupVal,
lookupType = lookup #2 #lookupType,
@@ -120,6 +118,13 @@
allFunct = all #6 #allFunct}
end;
+val local_context: use_context =
+ {tune_source = ML_Parse.fix_ints,
+ name_space = name_space,
+ str_of_pos = Position.str_of oo Position.line_file,
+ print = writeln,
+ error = error};
+
(* theorem bindings *)
@@ -134,7 +139,7 @@
else if not (ML_Syntax.is_identifier name) then
error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
else setmp stored_thms ths' (fn () =>
- use_text name_space (0, "") Output.ml_output true
+ use_text local_context (0, "") true
("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);")) ();
in () end;
@@ -214,12 +219,12 @@
fun no_decl _ = ([], []);
fun expand (Antiquote.Text tok) state = (K ([], [tok]), state)
- | expand (Antiquote.Antiq x) (scope, background) =
+ | expand (Antiquote.Antiq (ss, range)) (scope, background) =
let
val context = Stack.top scope;
- val (f, context') = antiquotation (T.read_antiq lex antiq x) context;
+ val (f, context') = antiquotation (T.read_antiq lex antiq (ss, #1 range)) context;
val (decl, background') = f {background = background, struct_name = struct_name};
- val decl' = pairself ML_Lex.tokenize o decl;
+ val decl' = decl #> pairself (ML_Lex.tokenize #> map (ML_Lex.set_range range));
in (decl', (Stack.map_top (K context') scope, background')) end
| expand (Antiquote.Open _) (scope, background) =
(no_decl, (Stack.push scope, background))
@@ -233,10 +238,10 @@
val trace = ref false;
-fun eval_wrapper pr verbose pos txt =
+fun eval verbose pos txt =
let
- fun eval_raw p = use_text name_space
- (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p)) pr;
+ fun eval_raw p = use_text local_context
+ (the_default 1 (Position.line_of p), the_default "ML" (Position.file_of p));
(*prepare source text*)
val _ = Position.report Markup.ML_source pos;
@@ -260,20 +265,18 @@
end;
-(* ML evaluation *)
+(* derived versions *)
-val eval = eval_wrapper Output.ml_output;
fun eval_file path = eval true (Path.position path) (File.read path);
fun eval_in ctxt verbose pos txt =
Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos txt) ();
-fun evaluate ctxt pr verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
+fun evaluate ctxt verbose (ref_name, r) txt = NAMED_CRITICAL "ML" (fn () =>
let
val _ = r := NONE;
val _ = Context.setmp_thread_data (SOME (Context.Proof ctxt)) (fn () =>
- eval_wrapper pr verbose Position.none
- ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))")) ();
+ eval verbose Position.none ("val _ = (" ^ ref_name ^ " := SOME (fn () => " ^ txt ^ "))")) ();
in (case ! r of NONE => error ("Bad evaluation for " ^ ref_name) | SOME e => e) end) ();
fun expression pos bind body txt =
--- a/src/Pure/ML/ml_lex.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML/ml_lex.ML Tue Mar 24 14:09:24 2009 +0100
@@ -13,6 +13,7 @@
val stopper: token Scan.stopper
val is_regular: token -> bool
val is_improper: token -> bool
+ val set_range: Position.range -> token -> token
val pos_of: token -> Position.T
val kind_of: token -> token_kind
val content_of: token -> string
@@ -42,6 +43,8 @@
(* position *)
+fun set_range range (Token (_, x)) = Token (range, x);
+
fun pos_of (Token ((pos, _), _)) = pos;
fun end_pos_of (Token ((_, pos), _)) = pos;
--- a/src/Pure/ML/ml_parse.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML/ml_parse.ML Tue Mar 24 14:09:24 2009 +0100
@@ -7,38 +7,38 @@
signature ML_PARSE =
sig
val fix_ints: string -> string
+ val global_context: use_context
end;
structure ML_Parse: ML_PARSE =
struct
-structure T = ML_Lex;
-
-
(** error handling **)
fun !!! scan =
let
fun get_pos [] = " (past end-of-file!)"
- | get_pos (tok :: _) = Position.str_of (T.pos_of tok);
+ | get_pos (tok :: _) = Position.str_of (ML_Lex.pos_of tok);
fun err (toks, NONE) = "SML syntax error" ^ get_pos toks
| err (toks, SOME msg) = "SML syntax error" ^ get_pos toks ^ ": " ^ msg;
in Scan.!! err scan end;
fun bad_input x =
- (Scan.some (fn tok => (case T.kind_of tok of T.Error msg => SOME msg | _ => NONE)) :|--
+ (Scan.some (fn tok => (case ML_Lex.kind_of tok of ML_Lex.Error msg => SOME msg | _ => NONE)) :|--
(fn msg => Scan.fail_with (K msg))) x;
(** basic parsers **)
fun $$$ x =
- Scan.one (fn tok => T.kind_of tok = T.Keyword andalso T.content_of tok = x) >> T.content_of;
-val int = Scan.one (fn tok => T.kind_of tok = T.Int) >> T.content_of;
+ Scan.one (fn tok => ML_Lex.kind_of tok = ML_Lex.Keyword andalso ML_Lex.content_of tok = x)
+ >> ML_Lex.content_of;
-val regular = Scan.one T.is_regular >> T.content_of;
-val improper = Scan.one T.is_improper >> T.content_of;
+val int = Scan.one (fn tok => ML_Lex.kind_of tok = ML_Lex.Int) >> ML_Lex.content_of;
+
+val regular = Scan.one ML_Lex.is_regular >> ML_Lex.content_of;
+val improper = Scan.one ML_Lex.is_improper >> ML_Lex.content_of;
val blanks = Scan.repeat improper >> implode;
@@ -55,11 +55,21 @@
fun do_fix_ints s =
Source.of_string s
- |> T.source
- |> Source.source T.stopper (Scan.bulk (!!! fix_int)) NONE
+ |> ML_Lex.source
+ |> Source.source ML_Lex.stopper (Scan.bulk (!!! fix_int)) NONE
|> Source.exhaust
|> implode;
val fix_ints = if ml_system_fix_ints then do_fix_ints else I;
+
+(* global use_context *)
+
+val global_context: use_context =
+ {tune_source = fix_ints,
+ name_space = ML_Name_Space.global,
+ str_of_pos = Position.str_of oo Position.line_file,
+ print = writeln,
+ error = error};
+
end;
--- a/src/Pure/ML/ml_test.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ML/ml_test.ML Tue Mar 24 14:09:24 2009 +0100
@@ -7,7 +7,7 @@
signature ML_TEST =
sig
val get_result: Proof.context -> PolyML.parseTree list
- val eval: bool -> bool -> Position.T -> ML_Lex.token list -> unit
+ val eval: bool -> Position.T -> ML_Lex.token list -> unit
end
structure ML_Test: ML_TEST =
@@ -25,9 +25,10 @@
val get_result = Result.get o Context.Proof;
-fun eval do_run verbose pos toks =
+
+fun use_text ({name_space = space, print, error, ...}: use_context) verbose pos toks =
let
- val (print, err) = Output.ml_output;
+ (* input *)
val input = toks |> map (fn tok =>
(serial (), (String.explode (ML_Lex.text_of tok), ML_Lex.pos_of tok)));
@@ -51,50 +52,106 @@
SOME c));
fun get_index () = (case ! in_buffer of [] => 0 | (i, _) :: _ => i);
+
+ (* output *)
+
val out_buffer = ref ([]: string list);
+ fun output () = implode (rev (! out_buffer));
fun put s = out_buffer := s :: ! out_buffer;
- fun output () = implode (rev (! out_buffer));
fun put_message {message, hard, location, context = _} =
(put (if hard then "Error: " else "Warning: ");
put (Pretty.string_of (Pretty.from_ML (pretty_ml message)));
put (Position.str_of (pos_of location) ^ "\n"));
+
+ (* results *)
+
+ fun apply_result {fixes, types, signatures, structures, functors, values} =
+ let
+ fun add_prefix prefix (PrettyBlock (ind, consistent, context, prts)) =
+ let
+ fun make_prefix context =
+ (case get_first (fn ContextParentStructure p => SOME p | _ => NONE) context of
+ SOME (name, sub_context) => make_prefix sub_context ^ name ^ "."
+ | NONE => prefix);
+ val this_prefix = make_prefix context;
+ in PrettyBlock (ind, consistent, context, map (add_prefix this_prefix) prts) end
+ | add_prefix prefix (prt as PrettyString s) =
+ if prefix = "" then prt else PrettyString (prefix ^ s)
+ | add_prefix _ (prt as PrettyBreak _) = prt;
+
+ val depth = get_print_depth ();
+ val with_struct = ! PolyML.Compiler.printTypesWithStructureName;
+
+ fun display disp x =
+ if depth > 0 then
+ (disp x
+ |> with_struct ? add_prefix ""
+ |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> put; put "\n")
+ else ();
+
+ fun apply_fix (a, b) =
+ (display PolyML.NameSpace.displayFix (a, b); #enterFix space (a, b));
+ fun apply_type (a, b) =
+ (display PolyML.NameSpace.displayType (b, depth); #enterType space (a, b));
+ fun apply_sig (a, b) =
+ (display PolyML.NameSpace.displaySig (b, depth, space); #enterSig space (a, b));
+ fun apply_struct (a, b) =
+ (display PolyML.NameSpace.displayStruct (b, depth, space); #enterStruct space (a, b));
+ fun apply_funct (a, b) =
+ (display PolyML.NameSpace.displayFunct (b, depth, space); #enterFunct space (a, b));
+ fun apply_val (a, b) =
+ (display PolyML.NameSpace.displayVal (b, depth, space); #enterVal space (a, b));
+ in
+ List.app apply_fix fixes;
+ List.app apply_type types;
+ List.app apply_sig signatures;
+ List.app apply_struct structures;
+ List.app apply_funct functors;
+ List.app apply_val values
+ end;
+
fun result_fun (parse_tree, code) () =
(Context.>> (Result.map (append (the_list parse_tree)));
- if is_none code then warning "Static Errors" else ());
+ (case code of NONE => error "Static Errors" | SOME result => apply_result (result ())));
+
+
+ (* compiler invocation *)
val parameters =
[PolyML.Compiler.CPOutStream put,
- PolyML.Compiler.CPNameSpace ML_Context.name_space,
+ PolyML.Compiler.CPNameSpace space,
PolyML.Compiler.CPErrorMessageProc put_message,
PolyML.Compiler.CPLineNo (fn () => ! current_line),
PolyML.Compiler.CPLineOffset get_index,
PolyML.Compiler.CPFileName (the_default "ML" (Position.file_of pos)),
- PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
- (if do_run then [] else [PolyML.Compiler.CPCompilerResultFun result_fun]);
+ PolyML.Compiler.CPPrintInAlphabeticalOrder false,
+ PolyML.Compiler.CPCompilerResultFun result_fun];
val _ =
(while not (List.null (! in_buffer)) do
PolyML.compiler (get, parameters) ())
handle exn =>
(put ("Exception- " ^ General.exnMessage exn ^ " raised");
- err (output ()); raise exn);
+ error (output ()); raise exn);
in if verbose then print (output ()) else () end;
+val eval = use_text ML_Context.local_context;
+
(* ML test command *)
-fun ML_test do_run (txt, pos) =
+fun ML_test (txt, pos) =
let
val _ = Position.report Markup.ML_source pos;
val ants = ML_Lex.read_antiq (Symbol_Pos.explode (txt, pos), pos);
val ((env, body), env_ctxt) = ML_Context.eval_antiquotes (ants, pos) (Context.thread_data ());
val _ = Context.setmp_thread_data env_ctxt
- (fn () => (eval true false Position.none env; Context.thread_data ())) ()
+ (fn () => (eval false Position.none env; Context.thread_data ())) ()
|> (fn NONE => () | SOME context' => Context.>> (ML_Context.inherit_env context'));
- val _ = eval do_run true pos body;
- val _ = eval true false Position.none (ML_Lex.tokenize "structure Isabelle = struct end");
+ val _ = eval true pos body;
+ val _ = eval false Position.none (ML_Lex.tokenize "structure Isabelle = struct end");
in () end;
@@ -107,12 +164,7 @@
val _ =
OuterSyntax.command "ML_test" "advanced ML compiler test" (K.tag_ml K.thy_decl)
(P.ML_source >> (fn src =>
- Toplevel.generic_theory (ML_Context.exec (fn () => ML_test true src) #> inherit_env)));
-
-val _ =
- OuterSyntax.command "ML_parse" "advanced ML compiler test (parse only)" (K.tag_ml K.thy_decl)
- (P.ML_source >> (fn src =>
- Toplevel.generic_theory (ML_Context.exec (fn () => ML_test false src) #> inherit_env)));
+ Toplevel.generic_theory (ML_Context.exec (fn () => ML_test src) #> inherit_env)));
end;
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Mar 24 14:09:24 2009 +0100
@@ -76,7 +76,7 @@
fun setup_messages () =
(Output.writeln_fn := message "" "" "";
- Output.status_fn := (fn s => ! Output.priority_fn s);
+ Output.status_fn := (fn _ => ());
Output.priority_fn := message (special "I") (special "J") "";
Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
Output.debug_fn := message (special "K") (special "L") "+++ ";
--- a/src/Pure/Thy/thy_output.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML Tue Mar 24 14:09:24 2009 +0100
@@ -148,8 +148,8 @@
fun eval_antiquote lex state (txt, pos) =
let
fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
- | expand (Antiquote.Antiq x) =
- let val (opts, src) = T.read_antiq lex antiq x in
+ | expand (Antiquote.Antiq (ss, (pos, _))) =
+ let val (opts, src) = T.read_antiq lex antiq (ss, pos) in
options opts (fn () => command src state) (); (*preview errors!*)
PrintMode.with_modes (! modes @ Latex.modes)
(Output.no_warnings (options opts (fn () => command src state))) ()
--- a/src/Tools/Compute_Oracle/am_compiler.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Tools/Compute_Oracle/am_compiler.ML Tue Mar 24 14:09:24 2009 +0100
@@ -185,7 +185,7 @@
in
compiled_rewriter := NONE;
- use_text ML_Context.name_space (1, "") Output.ml_output false (!buffer);
+ use_text ML_Context.local_context (1, "") false (!buffer);
case !compiled_rewriter of
NONE => raise (Compile "cannot communicate with compiled function")
| SOME r => (compiled_rewriter := NONE; r)
--- a/src/Tools/Compute_Oracle/am_sml.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Tools/Compute_Oracle/am_sml.ML Tue Mar 24 14:09:24 2009 +0100
@@ -492,7 +492,7 @@
fun writeTextFile name s = File.write (Path.explode name) s
-fun use_source src = use_text ML_Context.name_space (1, "") Output.ml_output false src
+fun use_source src = use_text ML_Context.local_context (1, "") false src
fun compile cache_patterns const_arity eqs =
let
--- a/src/Tools/code/code_ml.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Tools/code/code_ml.ML Tue Mar 24 14:09:24 2009 +0100
@@ -969,7 +969,7 @@
val (value_code, [SOME value_name']) = ml_code_of thy naming program' [value_name];
val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
^ space_implode " " (map (enclose "(" ")") args) ^ " end";
- in ML_Context.evaluate ctxt Output.ml_output false reff sml_code end;
+ in ML_Context.evaluate ctxt false reff sml_code end;
in eval'' thy (rpair eval') ct end;
fun eval_term reff = eval Code_Thingol.eval_term I reff;
@@ -1037,7 +1037,7 @@
fun isar_seri_sml module_name =
Code_Target.parse_args (Scan.succeed ())
#> (fn () => serialize_ml target_SML
- (SOME (use_text ML_Context.name_space (1, "generated code") Output.ml_output false))
+ (SOME (use_text ML_Context.local_context (1, "generated code") false))
pr_sml_module pr_sml_stmt module_name);
fun isar_seri_ocaml module_name =
--- a/src/Tools/nbe.ML Tue Mar 24 14:08:13 2009 +0100
+++ b/src/Tools/nbe.ML Tue Mar 24 14:09:24 2009 +0100
@@ -277,14 +277,12 @@
in
s
|> tracing (fn s => "\n--- code to be evaluated:\n" ^ s)
- |> ML_Context.evaluate ctxt
- (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n",
- Output.tracing o enclose "\n--- compiler echo (with error):\n" "\n---\n")
- (!trace) univs_cookie
+ |> ML_Context.evaluate ctxt (!trace) univs_cookie
|> (fn f => f deps_vals)
|> (fn univs => cs ~~ univs)
end;
+
(* preparing function equations *)
fun eqns_of_stmt (_, Code_Thingol.Fun (_, (_, []))) =