# HG changeset patch
# User wenzelm
# Date 1396791534 -7200
# Node ID 28b34e8e4a80d41951f1c7e0bdbc9dae1f0d9176
# Parent  7acc933bd7ccc0e0227b7449ddd4a0c5fc3e2b88
approximate ML antiquotation @{here} for Isabelle/Pure bootstrap;

diff -r 7acc933bd7cc -r 28b34e8e4a80 src/Pure/ML-Systems/compiler_polyml.ML
--- a/src/Pure/ML-Systems/compiler_polyml.ML	Sun Apr 06 15:19:22 2014 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml.ML	Sun Apr 06 15:38:54 2014 +0200
@@ -15,7 +15,8 @@
     (start_line, name) verbose txt =
   let
     val line = Unsynchronized.ref start_line;
-    val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
+    val in_buffer =
+      Unsynchronized.ref (String.explode (tune_source (ml_positions start_line name txt)));
     val out_buffer = Unsynchronized.ref ([]: string list);
     fun output () = drop_newline (implode (rev (! out_buffer)));
 
diff -r 7acc933bd7cc -r 28b34e8e4a80 src/Pure/ML-Systems/ml_positions.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_positions.ML	Sun Apr 06 15:38:54 2014 +0200
@@ -0,0 +1,16 @@
+(*  Title:      Pure/ML-Systems/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 " ^ 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 7acc933bd7cc -r 28b34e8e4a80 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Sun Apr 06 15:19:22 2014 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Sun Apr 06 15:38:54 2014 +0200
@@ -113,6 +113,7 @@
 (* ML compiler *)
 
 use "ML-Systems/use_context.ML";
+use "ML-Systems/ml_positions.ML";
 use "ML-Systems/compiler_polyml.ML";
 
 PolyML.Compiler.reportUnreferencedIds := true;
diff -r 7acc933bd7cc -r 28b34e8e4a80 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Sun Apr 06 15:19:22 2014 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Sun Apr 06 15:38:54 2014 +0200
@@ -20,6 +20,7 @@
 structure PolyML = struct end;
 use "ML-Systems/pp_dummy.ML";
 use "ML-Systems/use_context.ML";
+use "ML-Systems/ml_positions.ML";
 
 
 val seconds = Time.fromReal;
@@ -91,9 +92,10 @@
       in String.substring (str, 0, Int.max (0, size str - 1)) end;
   in
     Control.Print.out := out;
-    Backend.Interact.useStream (TextIO.openString (tune_source txt)) handle exn =>
-      (Control.Print.out := out_orig;
-        error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
+    Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line name txt)))
+      handle exn =>
+        (Control.Print.out := out_orig;
+          error ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
     Control.Print.out := out_orig;
     if verbose then print (output ()) else ()
   end;
diff -r 7acc933bd7cc -r 28b34e8e4a80 src/Pure/ROOT
--- a/src/Pure/ROOT	Sun Apr 06 15:19:22 2014 +0200
+++ b/src/Pure/ROOT	Sun Apr 06 15:38:54 2014 +0200
@@ -6,6 +6,7 @@
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/ml_name_space.ML"
+    "ML-Systems/ml_positions.ML"
     "ML-Systems/ml_pretty.ML"
     "ML-Systems/ml_system.ML"
     "ML-Systems/multithreading.ML"
@@ -30,6 +31,7 @@
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/ml_name_space.ML"
+    "ML-Systems/ml_positions.ML"
     "ML-Systems/ml_pretty.ML"
     "ML-Systems/ml_system.ML"
     "ML-Systems/multithreading.ML"