# HG changeset patch
# User wenzelm
# Date 1456244162 -3600
# Node ID 07bfd581495d61b33ed0e9e80164fccd9fbcc07f
# Parent  7891843d79bb9ca1282f4b2af9ac06d9cfb4582a# Parent  274f279c09e9dc1ad023464bc6765d130723571e
merged

diff -r 7891843d79bb -r 07bfd581495d Admin/polyml/build
--- a/Admin/polyml/build	Tue Feb 23 16:50:10 2016 +0100
+++ b/Admin/polyml/build	Tue Feb 23 17:16:02 2016 +0100
@@ -80,7 +80,7 @@
   cd "$SOURCE"
   make distclean
 
-  { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" "${USER_OPTIONS[@]}" && \
+  { ./configure --prefix="$PWD/$TARGET" "${OPTIONS[@]}" --enable-intinf-as-int "${USER_OPTIONS[@]}" && \
     make compiler && \
     make compiler && \
     make install; } || fail "Build failed"
diff -r 7891843d79bb -r 07bfd581495d lib/scripts/run-polyml-5.6
--- a/lib/scripts/run-polyml-5.6	Tue Feb 23 16:50:10 2016 +0100
+++ b/lib/scripts/run-polyml-5.6	Tue Feb 23 17:16:02 2016 +0100
@@ -63,7 +63,7 @@
   esac
 else
   check_file "$INFILE"
-  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Process.interruptConsoleProcesses ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
+  INIT="(Signal.signal (2, Signal.SIG_HANDLE (fn _ => Thread.Thread.broadcastInterrupt ())); PolyML.SaveState.loadState \"$PLATFORM_INFILE\" handle exn => (TextIO.output (TextIO.stdErr, General.exnMessage exn ^ \": $INFILE\\n\"); OS.Process.exit OS.Process.success));"
   EXIT=""
 fi
 
diff -r 7891843d79bb -r 07bfd581495d src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Pure/General/pretty.ML	Tue Feb 23 17:16:02 2016 +0100
@@ -375,14 +375,16 @@
 (** ML toplevel pretty printing **)
 
 fun to_ML (Block (m, consistent, indent, prts, _)) =
-      ML_Pretty.Block (m, consistent, indent, map to_ML prts)
-  | to_ML (Break b) = ML_Pretty.Break b
-  | to_ML (Str s) = ML_Pretty.String s;
+      ML_Pretty.Block (m, consistent, FixedInt.fromInt indent, map to_ML prts)
+  | to_ML (Break (force, wd, ind)) =
+      ML_Pretty.Break (force, FixedInt.fromInt wd, FixedInt.fromInt ind)
+  | to_ML (Str (s, len)) = ML_Pretty.String (s, FixedInt.fromInt len);
 
 fun from_ML (ML_Pretty.Block (m, consistent, indent, prts)) =
-      make_block m consistent indent (map from_ML prts)
-  | from_ML (ML_Pretty.Break b) = Break b
-  | from_ML (ML_Pretty.String s) = Str s;
+      make_block m consistent (FixedInt.toInt indent) (map from_ML prts)
+  | from_ML (ML_Pretty.Break (force, wd, ind)) =
+      Break (force, FixedInt.toInt wd, FixedInt.toInt ind)
+  | from_ML (ML_Pretty.String (s, len)) = Str (s, FixedInt.toInt len);
 
 end;
 
diff -r 7891843d79bb -r 07bfd581495d src/Pure/ML/exn_output.ML
--- a/src/Pure/ML/exn_output.ML	Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Pure/ML/exn_output.ML	Tue Feb 23 17:16:02 2016 +0100
@@ -19,6 +19,8 @@
   | SOME loc => Exn_Properties.position_of loc);
 
 fun pretty (exn: exn) =
-  Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (exn, ML_Options.get_print_depth ())));
+  Pretty.from_ML
+    (pretty_ml
+      (PolyML.prettyRepresentation (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
 
 end;
diff -r 7891843d79bb -r 07bfd581495d src/Pure/ML/exn_properties.ML
--- a/src/Pure/ML/exn_properties.ML	Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Pure/ML/exn_properties.ML	Tue Feb 23 17:16:02 2016 +0100
@@ -26,9 +26,9 @@
 
 fun position_of loc =
   Position.make
-   {line = #startLine loc,
-    offset = #startPosition loc,
-    end_offset = #endPosition loc,
+   {line = FixedInt.toInt (#startLine loc),
+    offset = FixedInt.toInt (#startPosition loc),
+    end_offset = FixedInt.toInt (#endPosition loc),
     props = props_of loc};
 
 
diff -r 7891843d79bb -r 07bfd581495d src/Pure/ML/install_pp_polyml.ML
--- a/src/Pure/ML/install_pp_polyml.ML	Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Pure/ML/install_pp_polyml.ML	Tue Feb 23 17:16:02 2016 +0100
@@ -59,10 +59,10 @@
   ml_pretty (Pretty.to_ML (Morphism.pretty morphism)));
 
 PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
-  ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
+  ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (FixedInt.toInt (depth * 100)) str)));
 
 PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
-  ml_pretty (Pretty.to_ML (XML.pretty depth tree)));
+  ml_pretty (Pretty.to_ML (XML.pretty (FixedInt.toInt depth) tree)));
 
 PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
   pretty (Synchronized.value var, depth));
@@ -87,13 +87,13 @@
 fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
 fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
 
-fun prt_term parens dp t =
+fun prt_term parens (dp: FixedInt.int) t =
   if dp <= 0 then Pretty.str "..."
   else
     (case t of
       _ $ _ =>
         op :: (strip_comb t)
-        |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
+        |> map_index (fn (i, u) => prt_term true (dp - FixedInt.fromInt i - 1) u)
         |> Pretty.separate " $"
         |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
     | Abs (a, T, b) =>
@@ -142,7 +142,8 @@
 and prt_proofs parens dp prf =
   let
     val (head, args) = strip_proof prf [];
-    val prts = head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - i - 2)) args);
+    val prts =
+      head (dp - 1) :: flat (map_index (fn (i, prt) => prt (dp - FixedInt.fromInt i - 2)) args);
   in if parens then Pretty.enclose "(" ")" prts else Pretty.block prts end
 
 and strip_proof (p % t) res =
diff -r 7891843d79bb -r 07bfd581495d src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Tue Feb 23 17:16:02 2016 +0100
@@ -201,7 +201,7 @@
 
     (* results *)
 
-    val depth = ML_Options.get_print_depth ();
+    val depth = FixedInt.fromInt (ML_Options.get_print_depth ());
 
     fun apply_result {fixes, types, signatures, structures, functors, values} =
       let
diff -r 7891843d79bb -r 07bfd581495d src/Pure/RAW/ROOT_polyml.ML
--- a/src/Pure/RAW/ROOT_polyml.ML	Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Tue Feb 23 17:16:02 2016 +0100
@@ -12,6 +12,9 @@
 then use "RAW/ml_name_space_polyml-5.6.ML"
 else use "RAW/ml_name_space_polyml.ML";
 
+if List.exists (fn (a, _) => a = "FixedInt") (#allStruct ML_Name_Space.global ()) then ()
+else use "RAW/fixed_int_dummy.ML";
+
 structure ML_Name_Space =
 struct
   open ML_Name_Space;
@@ -144,7 +147,8 @@
             val len' = property "length" len;
           in ML_Pretty.Block ((bg, en), consistent, ind, map (convert len') prts) end
       | convert len (PolyML.PrettyString s) =
-          ML_Pretty.String (s, case Int.fromString len of SOME i => i | NONE => size s)
+          ML_Pretty.String
+            (s, FixedInt.fromInt (case Int.fromString len of SOME i => i | NONE => size s))
   in convert "" end;
 
 fun ml_pretty (ML_Pretty.Break (false, width, offset)) = PolyML.PrettyBreak (width, offset)
@@ -157,9 +161,11 @@
         (if en = "" then [] else [PolyML.ContextProperty ("end", en)])
       in PolyML.PrettyBlock (ind, consistent, context, map ml_pretty prts) end
   | ml_pretty (ML_Pretty.String (s, len)) =
-      if len = size s then PolyML.PrettyString s
-      else PolyML.PrettyBlock
-        (0, false, [PolyML.ContextProperty ("length", Int.toString len)], [PolyML.PrettyString s]);
+      if len = FixedInt.fromInt (size s) then PolyML.PrettyString s
+      else
+        PolyML.PrettyBlock
+          (0, false,
+            [PolyML.ContextProperty ("length", FixedInt.toString len)], [PolyML.PrettyString s]);
 
 
 (* ML compiler *)
@@ -189,8 +195,8 @@
 then use "RAW/ml_parse_tree_polyml-5.6.ML" else ();
 
 fun ml_make_string struct_name =
-  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, " ^
-    struct_name ^ ".ML_print_depth ())))))";
+  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^
+    struct_name ^ ".ML_print_depth ()))))))";
 
 
 (* ML debugger *)
diff -r 7891843d79bb -r 07bfd581495d src/Pure/RAW/compiler_polyml.ML
--- a/src/Pure/RAW/compiler_polyml.ML	Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Pure/RAW/compiler_polyml.ML	Tue Feb 23 17:16:02 2016 +0100
@@ -29,7 +29,7 @@
      (put (if hard then "Error: " else "Warning: ");
       PolyML.prettyPrint (put, 76) msg1;
       (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
-      put ("At" ^ str_of_pos message_line file ^ "\n"));
+      put ("At" ^ str_of_pos (FixedInt.toInt message_line) file ^ "\n"));
 
     val parameters =
      [PolyML.Compiler.CPOutStream put,
diff -r 7891843d79bb -r 07bfd581495d src/Pure/RAW/fixed_int_dummy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/RAW/fixed_int_dummy.ML	Tue Feb 23 17:16:02 2016 +0100
@@ -0,0 +1,6 @@
+(*  Title:      Pure/RAW/fixed_int_dummy.ML
+
+FixedInt dummy that is not fixed (up to Poly/ML 5.6).
+*)
+
+structure FixedInt = IntInf;
diff -r 7891843d79bb -r 07bfd581495d src/Pure/RAW/ml_debugger_polyml-5.6.ML
--- a/src/Pure/RAW/ml_debugger_polyml-5.6.ML	Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Pure/RAW/ml_debugger_polyml-5.6.ML	Tue Feb 23 17:16:02 2016 +0100
@@ -44,7 +44,7 @@
 val _ =
   PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
     let val s = print_exn_id exn_id
-    in ml_pretty (ML_Pretty.String (s, size s)) end);
+    in ml_pretty (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
 
 
 (* hooks *)
diff -r 7891843d79bb -r 07bfd581495d src/Pure/RAW/ml_pretty.ML
--- a/src/Pure/RAW/ml_pretty.ML	Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Pure/RAW/ml_pretty.ML	Tue Feb 23 17:16:02 2016 +0100
@@ -8,23 +8,23 @@
 struct
 
 datatype pretty =
-  Block of (string * string) * bool * int * pretty list |
-  String of string * int |
-  Break of bool * int * int;
+  Block of (string * string) * bool * FixedInt.int * pretty list |
+  String of string * FixedInt.int |
+  Break of bool * FixedInt.int * FixedInt.int;
 
 fun block prts = Block (("", ""), false, 2, prts);
-fun str s = String (s, size s);
+fun str s = String (s, FixedInt.fromInt (size s));
 fun brk width = Break (false, width, 0);
 
-fun pair pretty1 pretty2 ((x, y), depth: int) =
+fun pair pretty1 pretty2 ((x, y), depth: FixedInt.int) =
   block [str "(", pretty1 (x, depth), str ",", brk 1, pretty2 (y, depth - 1), str ")"];
 
-fun enum sep lpar rpar pretty (args, depth) =
+fun enum sep lpar rpar pretty (args, depth: FixedInt.int) =
   let
     fun elems _ [] = []
       | elems 0 _ = [str "..."]
       | elems d [x] = [pretty (x, d)]
       | elems d (x :: xs) = pretty (x, d) :: str sep :: brk 1 :: elems (d - 1) xs;
-  in block (str lpar :: (elems (Int.max (depth, 0)) args @ [str rpar])) end;
+  in block (str lpar :: (elems (FixedInt.max (depth, 0)) args @ [str rpar])) end;
 
 end;
diff -r 7891843d79bb -r 07bfd581495d src/Pure/ROOT
--- a/src/Pure/ROOT	Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Pure/ROOT	Tue Feb 23 17:16:02 2016 +0100
@@ -9,6 +9,7 @@
     "RAW/compiler_polyml.ML"
     "RAW/exn.ML"
     "RAW/exn_trace_polyml-5.5.1.ML"
+    "RAW/fixed_int_dummy.ML"
     "RAW/ml_compiler_parameters.ML"
     "RAW/ml_compiler_parameters_polyml-5.6.ML"
     "RAW/ml_debugger.ML"
@@ -40,6 +41,7 @@
     "RAW/compiler_polyml.ML"
     "RAW/exn.ML"
     "RAW/exn_trace_polyml-5.5.1.ML"
+    "RAW/fixed_int_dummy.ML"
     "RAW/ml_compiler_parameters.ML"
     "RAW/ml_compiler_parameters_polyml-5.6.ML"
     "RAW/ml_debugger.ML"
diff -r 7891843d79bb -r 07bfd581495d src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Tue Feb 23 16:50:10 2016 +0100
+++ b/src/Pure/Tools/debugger.ML	Tue Feb 23 17:16:02 2016 +0100
@@ -189,7 +189,8 @@
     val space = ML_Debugger.debug_name_space (the_debug_state thread_name index);
 
     fun print x =
-      Pretty.from_ML (ML_Name_Space.display_val (x, ML_Options.get_print_depth (), space));
+      Pretty.from_ML
+        (ML_Name_Space.display_val (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space));
     fun print_all () =
       #allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
       |> sort_by #1 |> map (Pretty.item o single o print o #2)