1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Jul 23 16:37:17 2011 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Jul 23 17:22:28 2011 +0200
     1.3 @@ -1570,8 +1570,7 @@
     1.4  
     1.5  (* values_timeout configuration *)
     1.6  
     1.7 -val default_values_timeout =
     1.8 -  if String.isPrefix "smlnj" (getenv "ML_SYSTEM") then 600.0 else 20.0
     1.9 +val default_values_timeout = if ML_System.is_smlnj then 600.0 else 20.0
    1.10  
    1.11  val values_timeout = Attrib.setup_config_real @{binding values_timeout} (K default_values_timeout)
    1.12  

     2.1 --- a/src/Pure/General/sha1_polyml.ML	Sat Jul 23 16:37:17 2011 +0200
     2.2 +++ b/src/Pure/General/sha1_polyml.ML	Sat Jul 23 17:22:28 2011 +0200
     2.3 @@ -18,7 +18,7 @@
     2.4    in (op ^) (pairself hex_digit (Integer.div_mod (Char.ord c) 16)) end
     2.5  
     2.6  val lib_path =
     2.7 -  ("$ML_HOME/" ^ (if String.isSuffix "cygwin" ml_platform then "sha1.dll" else "libsha1.so"))
     2.8 +  ("$ML_HOME/" ^ (if ML_System.platform_is_cygwin then "sha1.dll" else "libsha1.so"))
     2.9    |> Path.explode;
    2.10  
    2.11  fun digest_external str =

     3.1 --- a/src/Pure/IsaMakefile	Sat Jul 23 16:37:17 2011 +0200
     3.2 +++ b/src/Pure/IsaMakefile	Sat Jul 23 17:22:28 2011 +0200
     3.3 @@ -26,6 +26,7 @@
     3.4    ML-Systems/compiler_polyml-5.3.ML			\
     3.5    ML-Systems/ml_name_space.ML				\
     3.6    ML-Systems/ml_pretty.ML				\
     3.7 +  ML-Systems/ml_system.ML				\
     3.8    ML-Systems/multithreading.ML				\
     3.9    ML-Systems/multithreading_polyml.ML			\
    3.10    ML-Systems/overloading_smlnj.ML			\

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/ML-Systems/ml_system.ML	Sat Jul 23 17:22:28 2011 +0200
     4.3 @@ -0,0 +1,27 @@
     4.4 +(*  Title:      Pure/ML-Systems/ml_system.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +ML system and platform information.
     4.8 +*)
     4.9 +
    4.10 +signature ML_SYSTEM =
    4.11 +sig
    4.12 +  val name: string
    4.13 +  val is_polyml: bool
    4.14 +  val is_smlnj: bool
    4.15 +  val platform: string
    4.16 +  val platform_is_cygwin: bool
    4.17 +end;
    4.18 +
    4.19 +structure ML_System: ML_SYSTEM =
    4.20 +struct
    4.21 +
    4.22 +val SOME name = OS.Process.getEnv "ML_SYSTEM";
    4.23 +val is_polyml = String.isPrefix "polyml" name;
    4.24 +val is_smlnj = String.isPrefix "smlnj" name;
    4.25 +
    4.26 +val SOME platform = OS.Process.getEnv "ML_PLATFORM";
    4.27 +val platform_is_cygwin = String.isSuffix "cygwin" platform;
    4.28 +
    4.29 +end;
    4.30 +

     5.1 --- a/src/Pure/ML-Systems/polyml-5.2.1.ML	Sat Jul 23 16:37:17 2011 +0200
     5.2 +++ b/src/Pure/ML-Systems/polyml-5.2.1.ML	Sat Jul 23 17:22:28 2011 +0200
     5.3 @@ -29,3 +29,5 @@
     5.4  use "ML-Systems/pp_polyml.ML";
     5.5  use "ML-Systems/pp_dummy.ML";
     5.6  
     5.7 +use "ML-Systems/ml_system.ML";
     5.8 +

     6.1 --- a/src/Pure/ML-Systems/polyml.ML	Sat Jul 23 16:37:17 2011 +0200
     6.2 +++ b/src/Pure/ML-Systems/polyml.ML	Sat Jul 23 17:22:28 2011 +0200
     6.3 @@ -71,3 +71,5 @@
     6.4  val ml_make_string =
     6.5    "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, get_print_depth ())))))";
     6.6  
     6.7 +use "ML-Systems/ml_system.ML";
     6.8 +

     7.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Sat Jul 23 16:37:17 2011 +0200
     7.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Jul 23 17:22:28 2011 +0200
     7.3 @@ -35,8 +35,6 @@
     7.4  
     7.5  (* Compiler options *)
     7.6  
     7.7 -val ml_system_fix_ints = false;
     7.8 -
     7.9  PolyML.Compiler.printInAlphabeticalOrder := false;
    7.10  PolyML.Compiler.maxInlineSize := 80;
    7.11  

     8.1 --- a/src/Pure/ML-Systems/proper_int.ML	Sat Jul 23 16:37:17 2011 +0200
     8.2 +++ b/src/Pure/ML-Systems/proper_int.ML	Sat Jul 23 17:22:28 2011 +0200
     8.3 @@ -5,8 +5,6 @@
     8.4  words.
     8.5  *)
     8.6  
     8.7 -val ml_system_fix_ints = true;
     8.8 -
     8.9  val mk_int = IntInf.fromInt: Int.int -> IntInf.int;
    8.10  val dest_int = IntInf.toInt: IntInf.int -> Int.int;
    8.11  

     9.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sat Jul 23 16:37:17 2011 +0200
     9.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sat Jul 23 17:22:28 2011 +0200
     9.3 @@ -159,3 +159,5 @@
     9.4  
     9.5  use "ML-Systems/unsynchronized.ML";
     9.6  
     9.7 +use "ML-Systems/ml_system.ML";
     9.8 +

    10.1 --- a/src/Pure/ML/ml_parse.ML	Sat Jul 23 16:37:17 2011 +0200
    10.2 +++ b/src/Pure/ML/ml_parse.ML	Sat Jul 23 17:22:28 2011 +0200
    10.3 @@ -53,14 +53,13 @@
    10.4    regular ||
    10.5    bad_input;
    10.6  
    10.7 -fun do_fix_ints s =
    10.8 -  Source.of_string s
    10.9 -  |> ML_Lex.source
   10.10 -  |> Source.source ML_Lex.stopper (Scan.bulk (!!! fix_int)) NONE
   10.11 -  |> Source.exhaust
   10.12 -  |> implode;
   10.13 -
   10.14 -val fix_ints = if ml_system_fix_ints then do_fix_ints else I;
   10.15 +val fix_ints =
   10.16 +  ML_System.is_smlnj ?
   10.17 +   (Source.of_string #>
   10.18 +    ML_Lex.source #>
   10.19 +    Source.source ML_Lex.stopper (Scan.bulk (!!! fix_int)) NONE #>
   10.20 +    Source.exhaust #>
   10.21 +    implode);
   10.22  
   10.23  
   10.24  (* global use_context *)

    11.1 --- a/src/Pure/ROOT.ML	Sat Jul 23 16:37:17 2011 +0200
    11.2 +++ b/src/Pure/ROOT.ML	Sat Jul 23 17:22:28 2011 +0200
    11.3 @@ -62,9 +62,7 @@
    11.4  use "General/binding.ML";
    11.5  
    11.6  use "General/sha1.ML";
    11.7 -if String.isPrefix "polyml" ml_system
    11.8 -then use "General/sha1_polyml.ML"
    11.9 -else ();
   11.10 +if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
   11.11  
   11.12  
   11.13  (* concurrency within the ML runtime *)
   11.14 @@ -73,8 +71,7 @@
   11.15  if Multithreading.available then ()
   11.16  else use "Concurrent/single_assignment_sequential.ML";
   11.17  
   11.18 -if String.isPrefix "smlnj" ml_system then ()
   11.19 -else use "Concurrent/time_limit.ML";
   11.20 +if ML_System.is_smlnj then () else use "Concurrent/time_limit.ML";
   11.21  
   11.22  if Multithreading.available
   11.23  then use "Concurrent/bash.ML"
   11.24 @@ -191,7 +188,7 @@
   11.25  use "ML/ml_env.ML";
   11.26  use "Isar/runtime.ML";
   11.27  use "ML/ml_compiler.ML";
   11.28 -if ml_system = "polyml-5.2.1" orelse String.isPrefix "smlnj" ml_system then ()
   11.29 +if ML_System.name = "polyml-5.2.1" orelse ML_System.is_smlnj then ()
   11.30  else use "ML/ml_compiler_polyml-5.3.ML";
   11.31  use "ML/ml_context.ML";
   11.32  

    12.1 --- a/src/Pure/mk	Sat Jul 23 16:37:17 2011 +0200
    12.2 +++ b/src/Pure/mk	Sat Jul 23 17:22:28 2011 +0200
    12.3 @@ -88,8 +88,6 @@
    12.4    LOG="$LOGDIR/$ITEM"
    12.5  
    12.6    "$ISABELLE_PROCESS" \
    12.7 -    -e "val ml_system = \"$ML_SYSTEM\";" \
    12.8 -    -e "val ml_platform = \"$ML_PLATFORM\";" \
    12.9      -e "use\"$COMPAT\" handle _ => exit 1;" \
   12.10      -e "structure Isar = struct fun main () = () end;" \
   12.11      -e "ml_prompts \"ML> \" \"ML# \";" \
   12.12 @@ -110,8 +108,6 @@
   12.13    LOG="$LOGDIR/$ITEM"
   12.14  
   12.15    "$ISABELLE_PROCESS" \
   12.16 -    -e "val ml_system = \"$ML_SYSTEM\";" \
   12.17 -    -e "val ml_platform = \"$ML_PLATFORM\";" \
   12.18      -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
   12.19      -e "ml_prompts \"ML> \" \"ML# \";" \
   12.20      -f -q -w RAW_ML_SYSTEM Pure > "$LOG" 2>&1

    13.1 --- a/src/Pure/pure_setup.ML	Sat Jul 23 16:37:17 2011 +0200
    13.2 +++ b/src/Pure/pure_setup.ML	Sat Jul 23 17:22:28 2011 +0200
    13.3 @@ -36,9 +36,9 @@
    13.4  toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
    13.5  toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
    13.6  
    13.7 -if ml_system = "polyml-5.2.1"
    13.8 +if ML_System.name = "polyml-5.2.1"
    13.9  then use "ML/install_pp_polyml.ML"
   13.10 -else if String.isPrefix "polyml" ml_system
   13.11 +else if ML_System.is_polyml
   13.12  then use "ML/install_pp_polyml-5.3.ML"
   13.13  else ();
   13.14  

    14.1 --- a/src/Tools/WWW_Find/ROOT.ML	Sat Jul 23 16:37:17 2011 +0200
    14.2 +++ b/src/Tools/WWW_Find/ROOT.ML	Sat Jul 23 17:22:28 2011 +0200
    14.3 @@ -1,6 +1,5 @@
    14.4 -if String.isPrefix "polyml" ml_system
    14.5 -then 
    14.6 -  (use "unicode_symbols.ML";
    14.7 +if ML_System.is_polyml then
    14.8 + (use "unicode_symbols.ML";
    14.9    use "html_unicode.ML";
   14.10    use "mime.ML";
   14.11    use "http_status.ML";
   14.12 @@ -13,4 +12,4 @@
   14.13    use "html_templates.ML";
   14.14    use "find_theorems.ML";
   14.15    use "yxml_find_theorems.ML")
   14.16 -else ()
   14.17 +else ();