# HG changeset patch
# User wenzelm
# Date 1457010186 -3600
# Node ID f14f17e656a694c9d32c83da2d8b3fe13fb6d6b7
# Parent  19afb533028e7185c4915f4ca62a059e87c9d173
clarified modules;

diff -r 19afb533028e -r f14f17e656a6 src/Pure/RAW/ROOT_polyml.ML
--- a/src/Pure/RAW/ROOT_polyml.ML	Thu Mar 03 11:59:03 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Thu Mar 03 14:03:06 2016 +0100
@@ -12,19 +12,6 @@
 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;
-  val initial_val =
-    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
-      (#allVal global ());
-  val initial_type = #allType global ();
-  val initial_fixity = #allFix global ();
-  val initial_structure = #allStruct global ();
-  val initial_signature = #allSig global ();
-  val initial_functor = #allFunct global ();
-end;
-
 
 (* exceptions *)
 
@@ -103,7 +90,6 @@
   val display_val = ML_Pretty.from_polyml o displayVal;
 end;
 
-use "RAW/ml_positions.ML";
 use "RAW/ml_compiler0.ML";
 
 PolyML.Compiler.reportUnreferencedIds := true;
diff -r 19afb533028e -r f14f17e656a6 src/Pure/RAW/ml_compiler0.ML
--- a/src/Pure/RAW/ml_compiler0.ML	Thu Mar 03 11:59:03 2016 +0100
+++ b/src/Pure/RAW/ml_compiler0.ML	Thu Mar 03 14:03:06 2016 +0100
@@ -31,6 +31,16 @@
   if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
   else s;
 
+fun ml_positions start_line name txt =
+  let
+    fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
+          let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
+          in positions line cs (s :: res) end
+      | positions line (c :: cs) res =
+          positions (if c = #"\n" then line + 1 else line) cs (str c :: res)
+      | positions _ [] res = rev res;
+  in String.concat (positions start_line (String.explode txt) []) end;
+
 fun use_text ({name_space, here, print, error, ...}: context) {line, file, verbose, debug} text =
   let
     val _ = Secure.deny_ml ();
diff -r 19afb533028e -r f14f17e656a6 src/Pure/RAW/ml_name_space.ML
--- a/src/Pure/RAW/ml_name_space.ML	Thu Mar 03 11:59:03 2016 +0100
+++ b/src/Pure/RAW/ml_name_space.ML	Thu Mar 03 14:03:06 2016 +0100
@@ -15,19 +15,27 @@
   type valueVal = Values.value;
   fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
   fun displayTypeExpression (x, depth, space) = Values.printType (x, depth, SOME space);
+  val initial_val =
+    List.filter (fn (a, _) => a <> "use" andalso a <> "exit" andalso a <> "commit")
+      (#allVal global ());
 
   type typeVal = TypeConstrs.typeConstr;
   fun displayType (x, depth, space) = TypeConstrs.print (x, depth, SOME space);
+  val initial_type = #allType global ();
 
   type fixityVal = Infixes.fixity;
   fun displayFix (_: string, x) = Infixes.print x;
+  val initial_fixity = #allFix global ();
 
   type structureVal = Structures.structureVal;
   fun displayStruct (x, depth, space) = Structures.print (x, depth, SOME space);
+  val initial_structure = #allStruct global ();
 
   type signatureVal = Signatures.signatureVal;
   fun displaySig (x, depth, space) = Signatures.print (x, depth, SOME space);
+  val initial_signature = #allSig global ();
 
   type functorVal = Functors.functorVal;
   fun displayFunct (x, depth, space) = Functors.print (x, depth, SOME space);
+  val initial_functor = #allFunct global ();
 end;
diff -r 19afb533028e -r f14f17e656a6 src/Pure/RAW/ml_positions.ML
--- a/src/Pure/RAW/ml_positions.ML	Thu Mar 03 11:59:03 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  Title:      Pure/RAW/ml_positions.ML
-    Author:     Makarius
-
-Approximate ML antiquotation @{here} for Isabelle/Pure bootstrap.
-*)
-
-fun ml_positions start_line name txt =
-  let
-    fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
-          let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
-          in positions line cs (s :: res) end
-      | positions line (c :: cs) res =
-          positions (if c = #"\n" then line + 1 else line) cs (str c :: res)
-      | positions _ [] res = rev res;
-  in String.concat (positions start_line (String.explode txt) []) end;
-
diff -r 19afb533028e -r f14f17e656a6 src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Mar 03 11:59:03 2016 +0100
+++ b/src/Pure/ROOT	Thu Mar 03 14:03:06 2016 +0100
@@ -11,7 +11,6 @@
     "RAW/ml_debugger.ML"
     "RAW/ml_heap.ML"
     "RAW/ml_name_space.ML"
-    "RAW/ml_positions.ML"
     "RAW/ml_pretty.ML"
     "RAW/ml_profiling.ML"
     "RAW/ml_system.ML"
@@ -30,7 +29,6 @@
     "RAW/ml_debugger.ML"
     "RAW/ml_heap.ML"
     "RAW/ml_name_space.ML"
-    "RAW/ml_positions.ML"
     "RAW/ml_pretty.ML"
     "RAW/ml_profiling.ML"
     "RAW/ml_system.ML"
diff -r 19afb533028e -r f14f17e656a6 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Thu Mar 03 11:59:03 2016 +0100
+++ b/src/Pure/Tools/debugger.ML	Thu Mar 03 14:03:06 2016 +0100
@@ -190,7 +190,8 @@
 
     fun print x =
       Pretty.from_ML
-        (ML_Name_Space.display_val (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space));
+        (ML_Pretty.from_polyml
+          (ML_Name_Space.displayVal (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)