--- a/src/Pure/Concurrent/future.ML Thu Sep 06 16:50:00 2018 +0200
+++ b/src/Pure/Concurrent/future.ML Thu Sep 06 16:50:16 2018 +0200
@@ -112,8 +112,8 @@
val _ =
ML_system_pp (fn depth => fn pretty => fn x =>
(case peek x of
- NONE => PolyML_Pretty.PrettyString "<future>"
- | SOME (Exn.Exn _) => PolyML_Pretty.PrettyString "<failed>"
+ NONE => PolyML.PrettyString "<future>"
+ | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
| SOME (Exn.Res y) => pretty (y, depth)));
--- a/src/Pure/Concurrent/lazy.ML Thu Sep 06 16:50:00 2018 +0200
+++ b/src/Pure/Concurrent/lazy.ML Thu Sep 06 16:50:16 2018 +0200
@@ -157,8 +157,8 @@
val _ =
ML_system_pp (fn depth => fn pretty => fn x =>
(case peek x of
- NONE => PolyML_Pretty.PrettyString "<lazy>"
- | SOME (Exn.Exn _) => PolyML_Pretty.PrettyString "<failed>"
+ NONE => PolyML.PrettyString "<lazy>"
+ | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
| SOME (Exn.Res y) => pretty (y, depth)));
end;
--- a/src/Pure/General/pretty.ML Thu Sep 06 16:50:00 2018 +0200
+++ b/src/Pure/General/pretty.ML Thu Sep 06 16:50:16 2018 +0200
@@ -76,8 +76,8 @@
val writeln_chunks2: T list -> unit
val to_ML: FixedInt.int -> T -> ML_Pretty.pretty
val from_ML: ML_Pretty.pretty -> T
- val to_polyml: T -> PolyML_Pretty.pretty
- val from_polyml: PolyML_Pretty.pretty -> T
+ val to_polyml: T -> PolyML.pretty
+ val from_polyml: PolyML.pretty -> T
end;
structure Pretty: PRETTY =
--- a/src/Pure/ML/ml_env.ML Thu Sep 06 16:50:00 2018 +0200
+++ b/src/Pure/ML/ml_env.ML Thu Sep 06 16:50:16 2018 +0200
@@ -18,7 +18,8 @@
val inherit: Context.generic list -> Context.generic -> Context.generic
type operations =
{read_source: Input.source -> ML_Lex.token Antiquote.antiquote list,
- explode_token: ML_Lex.token -> char list}
+ explode_token: ML_Lex.token -> char list,
+ ML_system: bool}
type environment = {read: string, write: string}
val parse_environment: Context.generic option -> string -> environment
val print_environment: environment -> string
@@ -86,6 +87,9 @@
Symtab.merge (K true) (signature1, signature2),
Symtab.merge (K true) (functor1, functor2));
+fun update_tables_values vals (val1, type1, fixity1, structure1, signature1, functor1) : tables =
+ (fold Symtab.update vals val1, type1, fixity1, structure1, signature1, functor1);
+
val sml_tables: tables =
(Symtab.make ML_Name_Space.sml_val,
Symtab.make ML_Name_Space.sml_type,
@@ -99,7 +103,8 @@
type operations =
{read_source: Input.source -> ML_Lex.token Antiquote.antiquote list,
- explode_token: ML_Lex.token -> char list};
+ explode_token: ML_Lex.token -> char list,
+ ML_system: bool};
local
@@ -176,22 +181,30 @@
(* setup operations *)
+val ML_system_values =
+ #allVal (ML_Name_Space.global) ()
+ |> filter (member (op =) ["ML_system_pretty", "ML_system_pp", "ML_system_overload"] o #1);
+
fun setup env_name ops thy =
thy |> (Context.theory_map o Data.map o apfst) (fn envs =>
let
val thy' = Sign.map_naming (K Name_Space.global_naming) thy;
- val tables = if env_name = Isabelle then empty_tables else sml_tables;
+ val tables =
+ (if env_name = Isabelle then empty_tables else sml_tables)
+ |> #ML_system ops ? update_tables_values ML_system_values;
val (_, envs') =
Name_Space.define (Context.Theory thy') true (Binding.name env_name, (tables, ops)) envs;
in envs' end);
val Isabelle_operations: operations =
{read_source = ML_Lex.read_source,
- explode_token = ML_Lex.check_content_of #> Symbol.explode #> maps (Symbol.esc #> String.explode)};
+ explode_token = ML_Lex.check_content_of #> Symbol.explode #> maps (Symbol.esc #> String.explode),
+ ML_system = false};
val SML_operations: operations =
{read_source = ML_Lex.read_source_sml,
- explode_token = ML_Lex.check_content_of #> String.explode};
+ explode_token = ML_Lex.check_content_of #> String.explode,
+ ML_system = false};
val _ = Theory.setup (setup Isabelle Isabelle_operations #> setup SML SML_operations);
--- a/src/Pure/ML/ml_init.ML Thu Sep 06 16:50:00 2018 +0200
+++ b/src/Pure/ML/ml_init.ML Thu Sep 06 16:50:16 2018 +0200
@@ -4,12 +4,6 @@
Initial ML environment.
*)
-structure PolyML_Pretty =
-struct
- datatype context = datatype PolyML.context;
- datatype pretty = datatype PolyML.pretty;
-end;
-
val seconds = Time.fromReal;
val _ =
--- a/src/Pure/ML/ml_pretty.ML Thu Sep 06 16:50:00 2018 +0200
+++ b/src/Pure/ML/ml_pretty.ML Thu Sep 06 16:50:16 2018 +0200
@@ -17,12 +17,12 @@
('a * 'b) * FixedInt.int -> pretty
val enum: string -> string -> string -> ('a * FixedInt.int -> pretty) ->
'a list * FixedInt.int -> pretty
- val to_polyml: pretty -> PolyML_Pretty.pretty
- val from_polyml: PolyML_Pretty.pretty -> pretty
- val format_polyml: int -> PolyML_Pretty.pretty -> string
+ val to_polyml: pretty -> PolyML.pretty
+ val from_polyml: PolyML.pretty -> pretty
+ val format_polyml: int -> PolyML.pretty -> string
val format: int -> pretty -> string
val default_margin: int
- val string_of_polyml: PolyML_Pretty.pretty -> string
+ val string_of_polyml: PolyML.pretty -> string
val make_string_fn: string
end;
@@ -54,39 +54,39 @@
(* convert *)
-fun to_polyml (Break (false, width, offset)) = PolyML_Pretty.PrettyBreak (width, offset)
+fun to_polyml (Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
| to_polyml (Break (true, _, _)) =
- PolyML_Pretty.PrettyBlock (0, false, [PolyML_Pretty.ContextProperty ("fbrk", "")],
- [PolyML_Pretty.PrettyString " "])
+ PolyML.PrettyBlock (0, false, [PolyML.ContextProperty ("fbrk", "")],
+ [PolyML.PrettyString " "])
| to_polyml (Block ((bg, en), consistent, ind, prts)) =
let val context =
- (if bg = "" then [] else [PolyML_Pretty.ContextProperty ("begin", bg)]) @
- (if en = "" then [] else [PolyML_Pretty.ContextProperty ("end", en)])
- in PolyML_Pretty.PrettyBlock (ind, consistent, context, map to_polyml prts) end
+ (if bg = "" then [] else [PolyML.ContextProperty ("begin", bg)]) @
+ (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
+ in PolyML.PrettyBlock (ind, consistent, context, map to_polyml prts) end
| to_polyml (String (s, len)) =
- if len = FixedInt.fromInt (size s) then PolyML_Pretty.PrettyString s
+ if len = FixedInt.fromInt (size s) then PolyML.PrettyString s
else
- PolyML_Pretty.PrettyBlock
+ PolyML.PrettyBlock
(0, false,
- [PolyML_Pretty.ContextProperty ("length", FixedInt.toString len)], [PolyML_Pretty.PrettyString s]);
+ [PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]);
val from_polyml =
let
- fun convert _ (PolyML_Pretty.PrettyBreak (width, offset)) = Break (false, width, offset)
- | convert _ (PolyML_Pretty.PrettyBlock (_, _,
- [PolyML_Pretty.ContextProperty ("fbrk", _)], [PolyML_Pretty.PrettyString " "])) =
+ fun convert _ (PolyML.PrettyBreak (width, offset)) = Break (false, width, offset)
+ | convert _ (PolyML.PrettyBlock (_, _,
+ [PolyML.ContextProperty ("fbrk", _)], [PolyML.PrettyString " "])) =
Break (true, 1, 0)
- | convert len (PolyML_Pretty.PrettyBlock (ind, consistent, context, prts)) =
+ | convert len (PolyML.PrettyBlock (ind, consistent, context, prts)) =
let
fun property name default =
- (case List.find (fn PolyML_Pretty.ContextProperty (a, _) => name = a | _ => false) context of
- SOME (PolyML_Pretty.ContextProperty (_, b)) => b
+ (case List.find (fn PolyML.ContextProperty (a, _) => name = a | _ => false) context of
+ SOME (PolyML.ContextProperty (_, b)) => b
| _ => default);
val bg = property "begin" "";
val en = property "end" "";
val len' = property "length" len;
in Block ((bg, en), consistent, ind, map (convert len') prts) end
- | convert len (PolyML_Pretty.PrettyString s) =
+ | convert len (PolyML.PrettyString s) =
String (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
in convert "" end;
--- a/src/Pure/ML_Bootstrap.thy Thu Sep 06 16:50:00 2018 +0200
+++ b/src/Pure/ML_Bootstrap.thy Thu Sep 06 16:50:16 2018 +0200
@@ -18,7 +18,7 @@
structure Output_Primitives = Output_Primitives_Virtual;
structure Thread_Data = Thread_Data_Virtual;
structure PolyML = PolyML;
- fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML_Pretty.pretty) = ();
+ fun ML_system_pp (_: FixedInt.int -> 'a -> 'b -> PolyML.pretty) = ();
Proofterm.proofs := 0;
@@ -29,6 +29,8 @@
struct
val pointerEq = pointer_eq;
structure IntInf = PolyML.IntInf;
+ datatype context = datatype PolyML.context;
+ datatype pretty = datatype PolyML.pretty;
end;
\<close>
\<close>