# HG changeset patch
# User wenzelm
# Date 1311434548 -7200
# Node ID 8f5add916a9933ba6955c5ce6b03961966570702
# Parent  9b00f09f77214c19c72049b1bb8bf4a9e9ccad5d
explicit structure ML_System;
tunned ML bootstrap;

diff -r 9b00f09f7721 -r 8f5add916a99 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Jul 23 16:37:17 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Jul 23 17:22:28 2011 +0200
@@ -1570,8 +1570,7 @@
 
 (* values_timeout configuration *)
 
-val default_values_timeout =
-  if String.isPrefix "smlnj" (getenv "ML_SYSTEM") then 600.0 else 20.0
+val default_values_timeout = if ML_System.is_smlnj then 600.0 else 20.0
 
 val values_timeout = Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout)
 
diff -r 9b00f09f7721 -r 8f5add916a99 src/Pure/General/sha1_polyml.ML
--- a/src/Pure/General/sha1_polyml.ML	Sat Jul 23 16:37:17 2011 +0200
+++ b/src/Pure/General/sha1_polyml.ML	Sat Jul 23 17:22:28 2011 +0200
@@ -18,7 +18,7 @@
   in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end
 
 val lib_path =
-  ("$ML_HOME/" ^ (if String.isSuffix "cygwin" ml_platform then "sha1.dll" else "libsha1.so"))
+  ("$ML_HOME/" ^ (if ML_System.platform_is_cygwin then "sha1.dll" else "libsha1.so"))
   |> Path.explode;
 
 fun digest_external str =
diff -r 9b00f09f7721 -r 8f5add916a99 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sat Jul 23 16:37:17 2011 +0200
+++ b/src/Pure/IsaMakefile	Sat Jul 23 17:22:28 2011 +0200
@@ -26,6 +26,7 @@
   ML-Systems/compiler_polyml-5.3.ML			\
   ML-Systems/ml_name_space.ML				\
   ML-Systems/ml_pretty.ML				\
+  ML-Systems/ml_system.ML				\
   ML-Systems/multithreading.ML				\
   ML-Systems/multithreading_polyml.ML			\
   ML-Systems/overloading_smlnj.ML			\
diff -r 9b00f09f7721 -r 8f5add916a99 src/Pure/ML-Systems/ml_system.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_system.ML	Sat Jul 23 17:22:28 2011 +0200
@@ -0,0 +1,27 @@
+(*  Title:      Pure/ML-Systems/ml_system.ML
+    Author:     Makarius
+
+ML system and platform information.
+*)
+
+signature ML_SYSTEM =
+sig
+  val name: string
+  val is_polyml: bool
+  val is_smlnj: bool
+  val platform: string
+  val platform_is_cygwin: bool
+end;
+
+structure ML_System: ML_SYSTEM =
+struct
+
+val SOME name = OS.Process.getEnv "ML_SYSTEM";
+val is_polyml = String.isPrefix "polyml" name;
+val is_smlnj = String.isPrefix "smlnj" name;
+
+val SOME platform = OS.Process.getEnv "ML_PLATFORM";
+val platform_is_cygwin = String.isSuffix "cygwin" platform;
+
+end;
+
diff -r 9b00f09f7721 -r 8f5add916a99 src/Pure/ML-Systems/polyml-5.2.1.ML
--- a/src/Pure/ML-Systems/polyml-5.2.1.ML	Sat Jul 23 16:37:17 2011 +0200
+++ b/src/Pure/ML-Systems/polyml-5.2.1.ML	Sat Jul 23 17:22:28 2011 +0200
@@ -29,3 +29,5 @@
 use "ML-Systems/pp_polyml.ML";
 use "ML-Systems/pp_dummy.ML";
 
+use "ML-Systems/ml_system.ML";
+
diff -r 9b00f09f7721 -r 8f5add916a99 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Sat Jul 23 16:37:17 2011 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Sat Jul 23 17:22:28 2011 +0200
@@ -71,3 +71,5 @@
 val ml_make_string =
   "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, get_print_depth ())))))";
 
+use "ML-Systems/ml_system.ML";
+
diff -r 9b00f09f7721 -r 8f5add916a99 src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Sat Jul 23 16:37:17 2011 +0200
+++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Jul 23 17:22:28 2011 +0200
@@ -35,8 +35,6 @@
 
 (* Compiler options *)
 
-val ml_system_fix_ints = false;
-
 PolyML.Compiler.printInAlphabeticalOrder := false;
 PolyML.Compiler.maxInlineSize := 80;
 
diff -r 9b00f09f7721 -r 8f5add916a99 src/Pure/ML-Systems/proper_int.ML
--- a/src/Pure/ML-Systems/proper_int.ML	Sat Jul 23 16:37:17 2011 +0200
+++ b/src/Pure/ML-Systems/proper_int.ML	Sat Jul 23 17:22:28 2011 +0200
@@ -5,8 +5,6 @@
 words.
 *)
 
-val ml_system_fix_ints = true;
-
 val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
 val dest_int = IntInf.toInt: IntInf.int -> Int.int;
 
diff -r 9b00f09f7721 -r 8f5add916a99 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Sat Jul 23 16:37:17 2011 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Sat Jul 23 17:22:28 2011 +0200
@@ -159,3 +159,5 @@
 
 use "ML-Systems/unsynchronized.ML";
 
+use "ML-Systems/ml_system.ML";
+
diff -r 9b00f09f7721 -r 8f5add916a99 src/Pure/ML/ml_parse.ML
--- a/src/Pure/ML/ml_parse.ML	Sat Jul 23 16:37:17 2011 +0200
+++ b/src/Pure/ML/ml_parse.ML	Sat Jul 23 17:22:28 2011 +0200
@@ -53,14 +53,13 @@
   regular ||
   bad_input;
 
-fun do_fix_ints s =
-  Source.of_string s
-  |> 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;
+val fix_ints =
+  ML_System.is_smlnj ?
+   (Source.of_string #>
+    ML_Lex.source #>
+    Source.source ML_Lex.stopper (Scan.bulk (!!! fix_int)) NONE #>
+    Source.exhaust #>
+    implode);
 
 
 (* global use_context *)
diff -r 9b00f09f7721 -r 8f5add916a99 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Jul 23 16:37:17 2011 +0200
+++ b/src/Pure/ROOT.ML	Sat Jul 23 17:22:28 2011 +0200
@@ -62,9 +62,7 @@
 use "General/binding.ML";
 
 use "General/sha1.ML";
-if String.isPrefix "polyml" ml_system
-then use "General/sha1_polyml.ML"
-else ();
+if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
 
 
 (* concurrency within the ML runtime *)
@@ -73,8 +71,7 @@
 if Multithreading.available then ()
 else use "Concurrent/single_assignment_sequential.ML";
 
-if String.isPrefix "smlnj" ml_system then ()
-else use "Concurrent/time_limit.ML";
+if ML_System.is_smlnj then () else use "Concurrent/time_limit.ML";
 
 if Multithreading.available
 then use "Concurrent/bash.ML"
@@ -191,7 +188,7 @@
 use "ML/ml_env.ML";
 use "Isar/runtime.ML";
 use "ML/ml_compiler.ML";
-if ml_system = "polyml-5.2.1" orelse String.isPrefix "smlnj" ml_system then ()
+if ML_System.name = "polyml-5.2.1" orelse ML_System.is_smlnj then ()
 else use "ML/ml_compiler_polyml-5.3.ML";
 use "ML/ml_context.ML";
 
diff -r 9b00f09f7721 -r 8f5add916a99 src/Pure/mk
--- a/src/Pure/mk	Sat Jul 23 16:37:17 2011 +0200
+++ b/src/Pure/mk	Sat Jul 23 17:22:28 2011 +0200
@@ -88,8 +88,6 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE_PROCESS" \
-    -e "val ml_system = \"$ML_SYSTEM\";" \
-    -e "val ml_platform = \"$ML_PLATFORM\";" \
     -e "use\"$COMPAT\" handle _ => exit 1;" \
     -e "structure Isar = struct fun main () = () end;" \
     -e "ml_prompts \"ML> \" \"ML# \";" \
@@ -110,8 +108,6 @@
   LOG="$LOGDIR/$ITEM"
 
   "$ISABELLE_PROCESS" \
-    -e "val ml_system = \"$ML_SYSTEM\";" \
-    -e "val ml_platform = \"$ML_PLATFORM\";" \
     -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
     -e "ml_prompts \"ML> \" \"ML# \";" \
     -f -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1
diff -r 9b00f09f7721 -r 8f5add916a99 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Sat Jul 23 16:37:17 2011 +0200
+++ b/src/Pure/pure_setup.ML	Sat Jul 23 17:22:28 2011 +0200
@@ -36,9 +36,9 @@
 toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
 toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
 
-if ml_system = "polyml-5.2.1"
+if ML_System.name = "polyml-5.2.1"
 then use "ML/install_pp_polyml.ML"
-else if String.isPrefix "polyml" ml_system
+else if ML_System.is_polyml
 then use "ML/install_pp_polyml-5.3.ML"
 else ();
 
diff -r 9b00f09f7721 -r 8f5add916a99 src/Tools/WWW_Find/ROOT.ML
--- a/src/Tools/WWW_Find/ROOT.ML	Sat Jul 23 16:37:17 2011 +0200
+++ b/src/Tools/WWW_Find/ROOT.ML	Sat Jul 23 17:22:28 2011 +0200
@@ -1,6 +1,5 @@
-if String.isPrefix "polyml" ml_system
-then 
-  (use "unicode_symbols.ML";
+if ML_System.is_polyml then
+ (use "unicode_symbols.ML";
   use "html_unicode.ML";
   use "mime.ML";
   use "http_status.ML";
@@ -13,4 +12,4 @@
   use "html_templates.ML";
   use "find_theorems.ML";
   use "yxml_find_theorems.ML")
-else ()
+else ();