# HG changeset patch
# User wenzelm
# Date 1244311091 -7200
# Node ID 85e864045497acb811e2fdcd30b9774cfe919743
# Parent  0ae32184bde03d8fec1b530e8c0c52441c19f89c
report_parse_tree: ML_open, ML_struct;
eval: terminate input by explicit end token, to ensure that Poly/ML attaches proper position to last input token;
tuned;

diff -r 0ae32184bde0 -r 85e864045497 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sat Jun 06 19:58:11 2009 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sat Jun 06 19:58:11 2009 +0200
@@ -41,14 +41,16 @@
 
 fun report_parse_tree depth space =
   let
+    fun report_decl markup loc decl =
+      Position.report_text Markup.ML_ref (position_of loc)
+        (Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
     fun report loc (PolyML.PTtype types) =
           PolyML.NameSpace.displayTypeExpression (types, depth, space)
           |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
           |> Position.report_text Markup.ML_typing (position_of loc)
-      | report loc (PolyML.PTdeclaredAt decl) =
-          Markup.markup
-            (Markup.properties (Position.properties_of (position_of decl)) Markup.ML_def) ""
-          |> Position.report_text Markup.ML_ref (position_of loc)
+      | 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
       | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
       | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
       | report _ _ = ()
@@ -77,7 +79,11 @@
           (Position.reset_range (ML_Lex.pos_of tok));
       in ps ~~ map (String.explode o Symbol.esc) syms end);
 
-    val input_buffer = ref input;
+    val end_pos =
+      if null toks then Position.none
+      else ML_Lex.end_pos_of (List.last toks);
+
+    val input_buffer = ref (input @ [(end_pos, [#"\n"])]);
     val line = ref (the_default 1 (Position.line_of pos));
 
     fun get_offset () =
@@ -152,9 +158,10 @@
       PolyML.Compiler.CPNameSpace space,
       PolyML.Compiler.CPErrorMessageProc put_message,
       PolyML.Compiler.CPLineNo (fn () => ! line),
+      PolyML.Compiler.CPLineOffset get_offset,
       PolyML.Compiler.CPFileName location_props,
-      PolyML.Compiler.CPLineOffset get_offset,
-      PolyML.Compiler.CPCompilerResultFun result_fun];
+      PolyML.Compiler.CPCompilerResultFun result_fun,
+      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
     val _ =
       (while not (List.null (! input_buffer)) do
         PolyML.compiler (get, parameters) ())