report possible breakpoint positions;
authorwenzelm
Fri Jul 17 16:23:25 2015 +0200 (2015-07-17)
changeset 607444eba53a0ac3d
parent 60743 37d624a8b128
child 60745 d86b4cd0f1ec
report possible breakpoint positions;
src/Pure/ML-Systems/ml_debugger_dummy.ML
src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML
src/Pure/ML-Systems/ml_parse_tree.ML
src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
     1.1 --- a/src/Pure/ML-Systems/ml_debugger_dummy.ML	Fri Jul 17 16:03:11 2015 +0200
     1.2 +++ b/src/Pure/ML-Systems/ml_debugger_dummy.ML	Fri Jul 17 16:23:25 2015 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4    val on_entry: (string * location -> unit) option -> unit
     1.5    val on_exit: (string * location -> unit) option -> unit
     1.6    val on_exit_exception: (string * location -> exn -> unit) option -> unit
     1.7 -  val on_break_point: (location * bool Unsynchronized.ref -> unit) option -> unit
     1.8 +  val on_breakpoint: (location * bool Unsynchronized.ref -> unit) option -> unit
     1.9    type state
    1.10    val state: Thread.thread -> state list
    1.11    val debug_function: state -> string
    1.12 @@ -29,7 +29,7 @@
    1.13  fun on_entry _ = ();
    1.14  fun on_exit _ = ();
    1.15  fun on_exit_exception _ = ();
    1.16 -fun on_break_point _ = ();
    1.17 +fun on_breakpoint _ = ();
    1.18  
    1.19  
    1.20  (* debugger *)
     2.1 --- a/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Fri Jul 17 16:03:11 2015 +0200
     2.2 +++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML	Fri Jul 17 16:23:25 2015 +0200
     2.3 @@ -14,7 +14,7 @@
     2.4  val on_entry = PolyML.DebuggerInterface.setOnEntry;
     2.5  val on_exit = PolyML.DebuggerInterface.setOnExit;
     2.6  val on_exit_exception = PolyML.DebuggerInterface.setOnExitException;
     2.7 -val on_break_point = PolyML.DebuggerInterface.setOnBreakPoint;
     2.8 +val on_breakpoint = PolyML.DebuggerInterface.setOnBreakPoint;
     2.9  
    2.10  
    2.11  (* debugger operations *)
     3.1 --- a/src/Pure/ML-Systems/ml_parse_tree.ML	Fri Jul 17 16:03:11 2015 +0200
     3.2 +++ b/src/Pure/ML-Systems/ml_parse_tree.ML	Fri Jul 17 16:23:25 2015 +0200
     3.3 @@ -7,13 +7,13 @@
     3.4  signature ML_PARSE_TREE =
     3.5  sig
     3.6    val completions: PolyML.ptProperties -> string list option
     3.7 -  val break_point: PolyML.ptProperties -> bool Unsynchronized.ref option
     3.8 +  val breakpoint: PolyML.ptProperties -> bool Unsynchronized.ref option
     3.9  end;
    3.10  
    3.11  structure ML_Parse_Tree: ML_PARSE_TREE =
    3.12  struct
    3.13  
    3.14  fun completions _ = NONE;
    3.15 -fun break_point _ = NONE;
    3.16 +fun breakpoint _ = NONE;
    3.17  
    3.18  end;
    3.19 \ No newline at end of file
     4.1 --- a/src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML	Fri Jul 17 16:03:11 2015 +0200
     4.2 +++ b/src/Pure/ML-Systems/ml_parse_tree_polyml-5.5.3.ML	Fri Jul 17 16:23:25 2015 +0200
     4.3 @@ -10,7 +10,7 @@
     4.4  fun completions (PolyML.PTcompletions x) = SOME x
     4.5    | completions _ = NONE;
     4.6  
     4.7 -fun break_point (PolyML.PTbreakPoint x) = SOME x
     4.8 -  | break_point _ = NONE;
     4.9 +fun breakpoint (PolyML.PTbreakPoint x) = SOME x
    4.10 +  | breakpoint _ = NONE;
    4.11  
    4.12  end;
    4.13 \ No newline at end of file
     5.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Fri Jul 17 16:03:11 2015 +0200
     5.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Fri Jul 17 16:23:25 2015 +0200
     5.3 @@ -20,6 +20,9 @@
     5.4        | NONE => true);
     5.5      fun is_reported pos = is_visible andalso Position.is_reported pos;
     5.6  
     5.7 +
     5.8 +    (* syntax reports *)
     5.9 +
    5.10      fun reported_types loc types =
    5.11        let val pos = Exn_Properties.position_of loc in
    5.12          is_reported pos ?
    5.13 @@ -53,12 +56,12 @@
    5.14          else I
    5.15        end;
    5.16  
    5.17 -    fun reported loc (PolyML.PTtype types) = reported_types loc types
    5.18 +    fun reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
    5.19 +      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
    5.20 +      | reported loc (PolyML.PTtype types) = reported_types loc types
    5.21        | reported loc (PolyML.PTdeclaredAt decl) = reported_entity Markup.ML_defN loc decl
    5.22        | reported loc (PolyML.PTopenedAt decl) = reported_entity Markup.ML_openN loc decl
    5.23        | reported loc (PolyML.PTstructureAt decl) = reported_entity Markup.ML_structureN loc decl
    5.24 -      | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
    5.25 -      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
    5.26        | reported loc pt =
    5.27            (case ML_Parse_Tree.completions pt of
    5.28              SOME names => reported_completions loc names
    5.29 @@ -71,14 +74,34 @@
    5.30        persistent_reports
    5.31        |> map (fn (pos, markup, text) => Position.reported_text pos (markup ()) (text ()))
    5.32        |> Output.report;
    5.33 -  in
    5.34 -    if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
    5.35 -    then
    5.36 -      Execution.print
    5.37 -        {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
    5.38 -        output
    5.39 -    else output ()
    5.40 -  end;
    5.41 +    val _ =
    5.42 +      if not (null persistent_reports) andalso redirect andalso Multithreading.enabled ()
    5.43 +      then
    5.44 +        Execution.print
    5.45 +          {name = "ML_Compiler.report", pos = Position.thread_data (), pri = Task_Queue.urgent_pri}
    5.46 +          output
    5.47 +      else output ();
    5.48 +
    5.49 +
    5.50 +    (* breakpoints *)
    5.51 +
    5.52 +    fun breakpoints _ (PolyML.PTnextSibling tree) = breakpoints_tree (tree ())
    5.53 +      | breakpoints _ (PolyML.PTfirstChild tree) = breakpoints_tree (tree ())
    5.54 +      | breakpoints loc pt =
    5.55 +          (case ML_Parse_Tree.breakpoint pt of
    5.56 +            SOME b =>
    5.57 +              let val pos = Exn_Properties.position_of loc in
    5.58 +                if is_reported pos then
    5.59 +                  let val id = serial ();
    5.60 +                  in cons ((pos, Markup.ML_breakpoint id), (id, b)) end
    5.61 +                else I
    5.62 +              end
    5.63 +          | NONE => I)
    5.64 +    and breakpoints_tree (loc, props) = fold (breakpoints loc) props;
    5.65 +
    5.66 +    val all_breakpoints = rev (breakpoints_tree parse_tree []);
    5.67 +    val _ = Position.reports (map #1 all_breakpoints);
    5.68 +  in map #2 all_breakpoints end;
    5.69  
    5.70  
    5.71  (* eval ML source tokens *)
    5.72 @@ -114,7 +137,7 @@
    5.73        | [] => Position.none);
    5.74  
    5.75  
    5.76 -    (* output channels *)
    5.77 +    (* output *)
    5.78  
    5.79      val writeln_buffer = Unsynchronized.ref Buffer.empty;
    5.80      fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
    5.81 @@ -137,6 +160,8 @@
    5.82            Pretty.string_of (Pretty.from_ML (pretty_ml msg));
    5.83        in if hard then err txt else warn txt end;
    5.84  
    5.85 +    val breakpoints = Unsynchronized.ref ([]: (serial * bool Unsynchronized.ref) list);
    5.86 +
    5.87  
    5.88      (* results *)
    5.89  
    5.90 @@ -175,7 +200,8 @@
    5.91      fun result_fun (phase1, phase2) () =
    5.92       ((case phase1 of
    5.93          NONE => ()
    5.94 -      | SOME parse_tree => report_parse_tree (#redirect flags) depth space parse_tree);
    5.95 +      | SOME parse_tree =>
    5.96 +          breakpoints := report_parse_tree (#redirect flags) depth space parse_tree);
    5.97        (case phase2 of
    5.98          NONE => raise STATIC_ERRORS ()
    5.99        | SOME code =>
     6.1 --- a/src/Pure/PIDE/markup.ML	Fri Jul 17 16:03:11 2015 +0200
     6.2 +++ b/src/Pure/PIDE/markup.ML	Fri Jul 17 16:23:25 2015 +0200
     6.3 @@ -19,6 +19,8 @@
     6.4    val nameN: string
     6.5    val name: string -> T -> T
     6.6    val kindN: string
     6.7 +  val serialN: string
     6.8 +  val serial_properties: int -> Properties.T
     6.9    val instanceN: string
    6.10    val languageN: string
    6.11    val symbolsN: string
    6.12 @@ -107,6 +109,7 @@
    6.13    val ML_openN: string
    6.14    val ML_structureN: string
    6.15    val ML_typingN: string val ML_typing: T
    6.16 +  val ML_breakpointN: string val ML_breakpoint: int -> T
    6.17    val antiquotedN: string val antiquoted: T
    6.18    val antiquoteN: string val antiquote: T
    6.19    val ML_antiquotationN: string
    6.20 @@ -150,8 +153,6 @@
    6.21    val runningN: string val running: T
    6.22    val finishedN: string val finished: T
    6.23    val failedN: string val failed: T
    6.24 -  val serialN: string
    6.25 -  val serial_properties: int -> Properties.T
    6.26    val exec_idN: string
    6.27    val initN: string
    6.28    val statusN: string
    6.29 @@ -268,6 +269,9 @@
    6.30  
    6.31  val kindN = "kind";
    6.32  
    6.33 +val serialN = "serial";
    6.34 +fun serial_properties i = [(serialN, print_int i)];
    6.35 +
    6.36  val instanceN = "instance";
    6.37  
    6.38  
    6.39 @@ -420,7 +424,7 @@
    6.40  val (typingN, typing) = markup_elem "typing";
    6.41  
    6.42  
    6.43 -(* ML syntax *)
    6.44 +(* ML *)
    6.45  
    6.46  val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1";
    6.47  val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2";
    6.48 @@ -440,6 +444,8 @@
    6.49  val ML_structureN = "ML_structure";
    6.50  val (ML_typingN, ML_typing) = markup_elem "ML_typing";
    6.51  
    6.52 +val (ML_breakpointN, ML_breakpoint) = markup_int "ML_breakpoint" serialN;
    6.53 +
    6.54  
    6.55  (* antiquotations *)
    6.56  
    6.57 @@ -539,9 +545,6 @@
    6.58  
    6.59  (* messages *)
    6.60  
    6.61 -val serialN = "serial";
    6.62 -fun serial_properties i = [(serialN, print_int i)];
    6.63 -
    6.64  val exec_idN = "exec_id";
    6.65  
    6.66  val initN = "init";
     7.1 --- a/src/Pure/PIDE/markup.scala	Fri Jul 17 16:03:11 2015 +0200
     7.2 +++ b/src/Pure/PIDE/markup.scala	Fri Jul 17 16:23:25 2015 +0200
     7.3 @@ -42,6 +42,9 @@
     7.4    val KIND = "kind"
     7.5    val Kind = new Properties.String(KIND)
     7.6  
     7.7 +  val SERIAL = "serial"
     7.8 +  val Serial = new Properties.Long(SERIAL)
     7.9 +
    7.10    val INSTANCE = "instance"
    7.11    val Instance = new Properties.String(INSTANCE)
    7.12  
    7.13 @@ -69,6 +72,15 @@
    7.14        if (markup.name == name) Prop.unapply(markup.properties) else None
    7.15    }
    7.16  
    7.17 +  class Markup_Long(val name: String, prop: String)
    7.18 +  {
    7.19 +    private val Prop = new Properties.Long(prop)
    7.20 +
    7.21 +    def apply(i: Long): Markup = Markup(name, Prop(i))
    7.22 +    def unapply(markup: Markup): Option[Long] =
    7.23 +      if (markup.name == name) Prop.unapply(markup.properties) else None
    7.24 +  }
    7.25 +
    7.26  
    7.27    /* formal entities */
    7.28  
    7.29 @@ -231,7 +243,7 @@
    7.30    val TEXT_FOLD = "text_fold"
    7.31  
    7.32  
    7.33 -  /* ML syntax */
    7.34 +  /* ML */
    7.35  
    7.36    val ML_KEYWORD1 = "ML_keyword1"
    7.37    val ML_KEYWORD2 = "ML_keyword2"
    7.38 @@ -251,6 +263,9 @@
    7.39    val ML_STRUCTURE = "ML_structure"
    7.40    val ML_TYPING = "ML_typing"
    7.41  
    7.42 +  val ML_BREAKPOINT = "ML_breakpoint"
    7.43 +  val ML_Breakpoint = new Markup_Long(ML_BREAKPOINT, SERIAL)
    7.44 +
    7.45  
    7.46    /* outer syntax */
    7.47  
    7.48 @@ -341,9 +356,6 @@
    7.49  
    7.50    /* messages */
    7.51  
    7.52 -  val SERIAL = "serial"
    7.53 -  val Serial = new Properties.Long(SERIAL)
    7.54 -
    7.55    val INIT = "init"
    7.56    val STATUS = "status"
    7.57    val REPORT = "report"