# HG changeset patch
# User wenzelm
# Date 1294693404 -3600
# Node ID a7462e442e35363e86849d76b8fb53e5fd33b157
# Parent  967cbbc77abd99aa42bb752897728257c1161aef
refined report_parse_tree: reverse reports happen to produce proper type information for inlined @{term}, @{typ} etc.;
tuned offset_position_of;

diff -r 967cbbc77abd -r a7462e442e35 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon Jan 10 21:45:44 2011 +0100
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Mon Jan 10 22:03:24 2011 +0100
@@ -22,9 +22,9 @@
       {line = line, column = 0, offset = offset, end_offset = end_offset, props = props}
   end;
 
-fun offset_position_of loc =
-  let val pos = position_of loc
-  in if is_some (Position.offset_of pos) then pos else Position.none end;
+fun offset_position_of (loc: PolyML.location) =
+  if #startPosition loc > 0 then position_of loc
+  else Position.none;
 
 fun exn_position exn =
   (case PolyML.exceptionLocation exn of
@@ -47,18 +47,21 @@
     fun report_decl markup loc decl =
       report_text (offset_position_of loc) Markup.ML_ref
         (Markup.markup (Position.markup (position_of decl) markup) "");
+
     fun report loc (PolyML.PTtype types) =
-          PolyML.NameSpace.displayTypeExpression (types, depth, space)
-          |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
-          |> report_text (offset_position_of loc) Markup.ML_typing
-      | report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl
-      | report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl
-      | report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl
+          cons (fn () =>
+            PolyML.NameSpace.displayTypeExpression (types, depth, space)
+            |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
+            |> report_text (offset_position_of loc) Markup.ML_typing)
+      | report loc (PolyML.PTdeclaredAt decl) = cons (fn () => report_decl Markup.ML_def loc decl)
+      | report loc (PolyML.PTopenedAt decl) = cons (fn () => report_decl Markup.ML_open loc decl)
+      | report loc (PolyML.PTstructureAt decl) =
+          cons (fn () => report_decl Markup.ML_struct loc decl)
       | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
       | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
-      | report _ _ = ()
-    and report_tree (loc, props) = List.app (report loc) props;
-  in report_tree end;
+      | report _ _ = I
+    and report_tree (loc, props) = fold (report loc) props;
+  in fn tree => List.app (fn e => e ()) (report_tree tree []) end;
 
 
 (* eval ML source tokens *)