# HG changeset patch
# User wenzelm
# Date 1437143005 -7200
# Node ID 4eba53a0ac3ddddce3a876e5f8b1698ded03b1e3
# Parent  37d624a8b128c04c33fb4cf25478a559cae83226
report possible breakpoint positions;

diff -r 37d624a8b128 -r 4eba53a0ac3d src/Pure/ML-Systems/ml_debugger_dummy.ML
--- a/src/Pure/ML-Systems/ml_debugger_dummy.ML	Fri Jul 17 16:03:11 2015 +0200
+++ b/src/Pure/ML-Systems/ml_debugger_dummy.ML	Fri Jul 17 16:23:25 2015 +0200
@@ -10,7 +10,7 @@
   val on_entry: (string * location -> unit) option -> unit
   val on_exit: (string * location -> unit) option -> unit
   val on_exit_exception: (string * location -> exn -> unit) option -> unit
-  val on_break_point: (location * bool Unsynchronized.ref -> unit) option -> unit
+  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
   type state
   val state: Thread.thread -> state list
   val debug_function: state -> string
@@ -29,7 +29,7 @@
 fun on_entry _ = ();
 fun on_exit _ = ();
 fun on_exit_exception _ = ();
-fun on_break_point _ = ();
+fun on_breakpoint _ = ();
 
 
 (* debugger *)
diff -r 37d624a8b128 -r 4eba53a0ac3d src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML
--- a/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Fri Jul 17 16:03:11 2015 +0200
+++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Fri Jul 17 16:23:25 2015 +0200
@@ -14,7 +14,7 @@
 val on_entry = PolyML.DebuggerInterface.setOnEntry;
 val on_exit = PolyML.DebuggerInterface.setOnExit;
 val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
-val on_break_point = PolyML.DebuggerInterface.setOnBreakPoint;
+val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
 
 
 (* debugger operations *)
diff -r 37d624a8b128 -r 4eba53a0ac3d src/Pure/ML-Systems/ml_parse_tree.ML
--- a/src/Pure/ML-Systems/ml_parse_tree.ML	Fri Jul 17 16:03:11 2015 +0200
+++ b/src/Pure/ML-Systems/ml_parse_tree.ML	Fri Jul 17 16:23:25 2015 +0200
@@ -7,13 +7,13 @@
 signature ML_PARSE_TREE =
 sig
   val completions: PolyML.ptProperties -> string list option
-  val break_point: PolyML.ptProperties -> bool Unsynchronized.ref option
+  val breakpoint: PolyML.ptProperties -> bool Unsynchronized.ref option
 end;
 
 structure ML_Parse_Tree: ML_PARSE_TREE =
 struct
 
 fun completions _ = NONE;
-fun break_point _ = NONE;
+fun breakpoint _ = NONE;
 
 end;
\ No newline at end of file
diff -r 37d624a8b128 -r 4eba53a0ac3d src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML
--- a/src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML	Fri Jul 17 16:03:11 2015 +0200
+++ b/src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML	Fri Jul 17 16:23:25 2015 +0200
@@ -10,7 +10,7 @@
 fun completions (PolyML.PTcompletions x) = SOME x
   | completions _ = NONE;
 
-fun break_point (PolyML.PTbreakPoint x) = SOME x
-  | break_point _ = NONE;
+fun breakpoint (PolyML.PTbreakPoint x) = SOME x
+  | breakpoint _ = NONE;
 
 end;
\ No newline at end of file
diff -r 37d624a8b128 -r 4eba53a0ac3d src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Fri Jul 17 16:03:11 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Fri Jul 17 16:23:25 2015 +0200
@@ -20,6 +20,9 @@
       | NONE => true);
     fun is_reported pos = is_visible andalso Position.is_reported pos;
 
+
+    (* syntax reports *)
+
     fun reported_types loc types =
       let val pos = Exn_Properties.position_of loc in
         is_reported pos ?
@@ -53,12 +56,12 @@
         else I
       end;
 
-    fun reported loc (PolyML.PTtype types) = reported_types loc types
+    fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
+      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
+      | 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 loc pt =
           (case ML_Parse_Tree.completions pt of
             SOME names => reported_completions loc names
@@ -71,14 +74,34 @@
       persistent_reports
       |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
       |> Output.report;
-  in
-    if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
-    then
-      Execution.print
-        {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
-        output
-    else output ()
-  end;
+    val _ =
+      if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
+      then
+        Execution.print
+          {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
+          output
+      else output ();
+
+
+    (* breakpoints *)
+
+    fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ())
+      | breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ())
+      | breakpoints loc pt =
+          (case ML_Parse_Tree.breakpoint pt of
+            SOME b =>
+              let val pos = Exn_Properties.position_of loc in
+                if is_reported pos then
+                  let val id = serial ();
+                  in cons ((pos, Markup.ML_breakpoint id), (id, b)) end
+                else I
+              end
+          | NONE => I)
+    and breakpoints_tree (loc, props) = fold (breakpoints loc) props;
+
+    val all_breakpoints = rev (breakpoints_tree parse_tree []);
+    val _ = Position.reports (map #1 all_breakpoints);
+  in map #2 all_breakpoints end;
 
 
 (* eval ML source tokens *)
@@ -114,7 +137,7 @@
       | [] => Position.none);
 
 
-    (* output channels *)
+    (* output *)
 
     val writeln_buffer = Unsynchronized.ref Buffer.empty;
     fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
@@ -137,6 +160,8 @@
           Pretty.string_of (Pretty.from_ML (pretty_ml msg));
       in if hard then err txt else warn txt end;
 
+    val breakpoints = Unsynchronized.ref ([]: (serial * bool Unsynchronized.ref) list);
+
 
     (* results *)
 
@@ -175,7 +200,8 @@
     fun result_fun (phase1, phase2) () =
      ((case phase1 of
         NONE => ()
-      | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree);
+      | SOME parse_tree =>
+          breakpoints := report_parse_tree (#redirect flags) depth space parse_tree);
       (case phase2 of
         NONE => raise STATIC_ERRORS ()
       | SOME code =>
diff -r 37d624a8b128 -r 4eba53a0ac3d src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Jul 17 16:03:11 2015 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Jul 17 16:23:25 2015 +0200
@@ -19,6 +19,8 @@
   val nameN: string
   val name: string -> T -> T
   val kindN: string
+  val serialN: string
+  val serial_properties: int -> Properties.T
   val instanceN: string
   val languageN: string
   val symbolsN: string
@@ -107,6 +109,7 @@
   val ML_openN: string
   val ML_structureN: string
   val ML_typingN: string val ML_typing: T
+  val ML_breakpointN: string val ML_breakpoint: int -> T
   val antiquotedN: string val antiquoted: T
   val antiquoteN: string val antiquote: T
   val ML_antiquotationN: string
@@ -150,8 +153,6 @@
   val runningN: string val running: T
   val finishedN: string val finished: T
   val failedN: string val failed: T
-  val serialN: string
-  val serial_properties: int -> Properties.T
   val exec_idN: string
   val initN: string
   val statusN: string
@@ -268,6 +269,9 @@
 
 val kindN = "kind";
 
+val serialN = "serial";
+fun serial_properties i = [(serialN, print_int i)];
+
 val instanceN = "instance";
 
 
@@ -420,7 +424,7 @@
 val (typingN, typing) = markup_elem "typing";
 
 
-(* ML syntax *)
+(* ML *)
 
 val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1";
 val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2";
@@ -440,6 +444,8 @@
 val ML_structureN = "ML_structure";
 val (ML_typingN, ML_typing) = markup_elem "ML_typing";
 
+val (ML_breakpointN, ML_breakpoint) = markup_int "ML_breakpoint" serialN;
+
 
 (* antiquotations *)
 
@@ -539,9 +545,6 @@
 
 (* messages *)
 
-val serialN = "serial";
-fun serial_properties i = [(serialN, print_int i)];
-
 val exec_idN = "exec_id";
 
 val initN = "init";
diff -r 37d624a8b128 -r 4eba53a0ac3d src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Jul 17 16:03:11 2015 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Jul 17 16:23:25 2015 +0200
@@ -42,6 +42,9 @@
   val KIND = "kind"
   val Kind = new Properties.String(KIND)
 
+  val SERIAL = "serial"
+  val Serial = new Properties.Long(SERIAL)
+
   val INSTANCE = "instance"
   val Instance = new Properties.String(INSTANCE)
 
@@ -69,6 +72,15 @@
       if (markup.name == name) Prop.unapply(markup.properties) else None
   }
 
+  class Markup_Long(val name: String, prop: String)
+  {
+    private val Prop = new Properties.Long(prop)
+
+    def apply(i: Long): Markup = Markup(name, Prop(i))
+    def unapply(markup: Markup): Option[Long] =
+      if (markup.name == name) Prop.unapply(markup.properties) else None
+  }
+
 
   /* formal entities */
 
@@ -231,7 +243,7 @@
   val TEXT_FOLD = "text_fold"
 
 
-  /* ML syntax */
+  /* ML */
 
   val ML_KEYWORD1 = "ML_keyword1"
   val ML_KEYWORD2 = "ML_keyword2"
@@ -251,6 +263,9 @@
   val ML_STRUCTURE = "ML_structure"
   val ML_TYPING = "ML_typing"
 
+  val ML_BREAKPOINT = "ML_breakpoint"
+  val ML_Breakpoint = new Markup_Long(ML_BREAKPOINT, SERIAL)
+
 
   /* outer syntax */
 
@@ -341,9 +356,6 @@
 
   /* messages */
 
-  val SERIAL = "serial"
-  val Serial = new Properties.Long(SERIAL)
-
   val INIT = "init"
   val STATUS = "status"
   val REPORT = "report"