# HG changeset patch
# User wenzelm
# Date 1460729207 -7200
# Node ID 1de6405023a3769a5f7b21ec70526bf9239d2387
# Parent  d2e3b3b159d7c2b6d2a35ffd397fc8f7bc5d59ad
support for Poly/ML entity ids;

diff -r d2e3b3b159d7 -r 1de6405023a3 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Fri Apr 15 15:08:43 2016 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Fri Apr 15 16:06:47 2016 +0200
@@ -82,6 +82,17 @@
           in cons (pos, markup, fn () => "") end
       end;
 
+    fun reported_entity_id def id loc =
+      let
+        val pos = Exn_Properties.position_of_polyml_location loc;
+      in
+        is_reported pos ?
+          let
+            fun markup () =
+              (Markup.entityN, [(if def then Markup.defN else Markup.refN, Markup.print_int id)]);
+          in cons (pos, markup, fn () => "") end
+      end;
+
     fun reported_completions loc names =
       let val pos = Exn_Properties.position_of_polyml_location loc in
         if is_reported pos andalso not (null names) then
@@ -94,6 +105,8 @@
 
     fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
       | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
+      | reported loc (PolyML.PTdefId id) = reported_entity_id true (FixedInt.toLarge id) loc
+      | reported loc (PolyML.PTrefId id) = reported_entity_id false (FixedInt.toLarge id) loc
       | reported loc (PolyML.PTtype types) = reported_types loc types
       | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
       | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
@@ -268,7 +281,8 @@
       PolyML.Compiler.CPPrintDepth ML_Print_Depth.get_print_depth,
       PolyML.Compiler.CPCompilerResultFun result_fun,
       PolyML.Compiler.CPPrintInAlphabeticalOrder false,
-      PolyML.Compiler.CPDebug debug];
+      PolyML.Compiler.CPDebug debug,
+      PolyML.Compiler.CPBindingSeq serial];
 
     val _ =
       (while not (List.null (! input_buffer)) do