# HG changeset patch
# User wenzelm
# Date 1437050423 -7200
# Node ID 4ac4b314d93c79ae6613b8ac32d3a6ea810f4390
# Parent  02c2860fcf309fa6c5b2ad08b6cc702c572018a4
additional ML parse tree components for Poly/ML 5.5.3, or later;
support for ML completion;
tuned;

diff -r 02c2860fcf30 -r 4ac4b314d93c src/Pure/General/completion.ML
--- a/src/Pure/General/completion.ML	Thu Jul 16 11:38:18 2015 +0200
+++ b/src/Pure/General/completion.ML	Thu Jul 16 14:40:23 2015 +0200
@@ -10,6 +10,7 @@
   val names: Position.T -> (string * (string * string)) list -> T
   val none: T
   val make: string * Position.T -> ((string -> bool) -> (string * (string * string)) list) -> T
+  val encode: T -> XML.body
   val reported_text: T -> string
   val suppress_abbrevs: string -> Markup.T list
 end;
@@ -40,14 +41,18 @@
   then names pos (make_names (String.isPrefix (Name.clean name)))
   else none;
 
+fun encode completion =
+  let
+    val {total, names, ...} = dest completion;
+    open XML.Encode;
+  in pair int (list (pair string (pair string string))) (total, names) end;
+
 fun reported_text completion =
-  let val {pos, total, names} = dest completion in
+  let val {pos, names, ...} = dest completion in
     if Position.is_reported pos andalso not (null names) then
       let
         val markup = Position.markup pos Markup.completion;
-        val body = (total, names) |>
-          let open XML.Encode in pair int (list (pair string (pair string string))) end;
-      in YXML.string_of (XML.Elem (markup, body)) end
+      in YXML.string_of (XML.Elem (markup, encode completion)) end
     else ""
   end;
 
diff -r 02c2860fcf30 -r 4ac4b314d93c src/Pure/ML-Systems/ml_parse_tree.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_parse_tree.ML	Thu Jul 16 14:40:23 2015 +0200
@@ -0,0 +1,19 @@
+(*  Title:      Pure/ML/ml_parse_tree.ML
+    Author:     Makarius
+
+Additional ML parse tree components for Poly/ML.
+*)
+
+signature ML_PARSE_TREE =
+sig
+  val completions: PolyML.ptProperties -> string list option
+  val break_point: PolyML.ptProperties -> bool Unsynchronized.ref option
+end;
+
+structure ML_Parse_Tree: ML_PARSE_TREE =
+struct
+
+fun completions _ = NONE;
+fun break_point _ = NONE;
+
+end;
\ No newline at end of file
diff -r 02c2860fcf30 -r 4ac4b314d93c src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML	Thu Jul 16 14:40:23 2015 +0200
@@ -0,0 +1,16 @@
+(*  Title:      Pure/ML/ml_parse_tree_polyml-5.5.3.ML
+    Author:     Makarius
+
+Additional ML parse tree components for Poly/ML 5.5.3, or later.
+*)
+
+structure ML_Parse_Tree: ML_PARSE_TREE =
+struct
+
+fun completions (PolyML.PTcompletions x) = SOME x
+  | completions _ = NONE;
+
+fun break_point (PolyML.PTbreakPoint x) = SOME x
+  | break_point _ = NONE;
+
+end;
\ No newline at end of file
diff -r 02c2860fcf30 -r 4ac4b314d93c src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Jul 16 11:38:18 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Jul 16 14:40:23 2015 +0200
@@ -132,6 +132,9 @@
 
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
 
+use "ML-Systems/ml_parse_tree.ML";
+if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
+
 
 (* ML debugger *)
 
diff -r 02c2860fcf30 -r 4ac4b314d93c src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Thu Jul 16 11:38:18 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu Jul 16 14:40:23 2015 +0200
@@ -43,13 +43,26 @@
           in cons (pos, markup, fn () => "") end
       end;
 
+    fun reported_completions loc names =
+      let val pos = Exn_Properties.position_of loc in
+        if is_reported pos then
+          let
+            val completion = Completion.names pos (map (fn a => (a, ("ML", ""))) names);
+            val xml = Completion.encode completion;
+          in cons (pos, fn () => Markup.completion, fn () => YXML.string_of_body xml) end
+        else I
+      end;
+
     fun 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
       | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
       | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
       | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
-      | reported _ _ = I
+      | reported loc pt =
+          (case ML_Parse_Tree.completions pt of
+            SOME names => reported_completions loc names
+          | NONE => I)
     and reported_tree (loc, props) = fold (reported loc) props;
 
     val persistent_reports = reported_tree parse_tree [];
diff -r 02c2860fcf30 -r 4ac4b314d93c src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Jul 16 11:38:18 2015 +0200
+++ b/src/Pure/ROOT	Thu Jul 16 14:40:23 2015 +0200
@@ -9,20 +9,22 @@
     "ML-Systems/ml_debugger_dummy.ML"
     "ML-Systems/ml_debugger_polyml-5.5.3.ML"
     "ML-Systems/ml_name_space.ML"
+    "ML-Systems/ml_parse_tree.ML"
+    "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
     "ML-Systems/ml_positions.ML"
     "ML-Systems/ml_pretty.ML"
     "ML-Systems/ml_system.ML"
     "ML-Systems/multithreading.ML"
     "ML-Systems/multithreading_polyml.ML"
     "ML-Systems/overloading_smlnj.ML"
-    "ML-Systems/polyml.ML"
     "ML-Systems/polyml-5.5.2.ML"
     "ML-Systems/polyml-5.5.3.ML"
+    "ML-Systems/polyml.ML"
     "ML-Systems/pp_dummy.ML"
     "ML-Systems/proper_int.ML"
+    "ML-Systems/share_common_data_polyml-5.3.0.ML"
     "ML-Systems/single_assignment.ML"
     "ML-Systems/single_assignment_polyml.ML"
-    "ML-Systems/share_common_data_polyml-5.3.0.ML"
     "ML-Systems/smlnj.ML"
     "ML-Systems/thread_dummy.ML"
     "ML-Systems/universal.ML"
@@ -35,18 +37,23 @@
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
     "ML-Systems/exn_trace_polyml-5.5.1.ML"
+    "ML-Systems/ml_debugger_dummy.ML"
+    "ML-Systems/ml_debugger_polyml-5.5.3.ML"
     "ML-Systems/ml_name_space.ML"
+    "ML-Systems/ml_parse_tree.ML"
+    "ML-Systems/ml_parse_tree_polyml-5.5.3.ML"
     "ML-Systems/ml_positions.ML"
     "ML-Systems/ml_pretty.ML"
     "ML-Systems/ml_system.ML"
     "ML-Systems/multithreading.ML"
     "ML-Systems/multithreading_polyml.ML"
     "ML-Systems/overloading_smlnj.ML"
-    "ML-Systems/polyml.ML"
     "ML-Systems/polyml-5.5.2.ML"
     "ML-Systems/polyml-5.5.3.ML"
+    "ML-Systems/polyml.ML"
     "ML-Systems/pp_dummy.ML"
     "ML-Systems/proper_int.ML"
+    "ML-Systems/share_common_data_polyml-5.3.0.ML"
     "ML-Systems/single_assignment.ML"
     "ML-Systems/single_assignment_polyml.ML"
     "ML-Systems/smlnj.ML"