set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
authorwenzelm
Mon Aug 10 20:22:49 2015 +0200 (2015-08-10)
changeset 60880fa958e24ff24
parent 60879 3dc649cfd512
child 60881 91a9a4395903
set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
src/Pure/PIDE/document.ML
src/Pure/Tools/debugger.ML
src/Pure/Tools/debugger.scala
src/Tools/jEdit/src/debugger_dockable.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Aug 10 19:17:49 2015 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Aug 10 20:22:49 2015 +0200
     1.3 @@ -21,6 +21,7 @@
     1.4    type blob_digest = (string * string option) Exn.result
     1.5    val define_command: Document_ID.command -> string -> blob_digest list -> int ->
     1.6      ((int * int) * string) list -> state -> state
     1.7 +  val command_exec: state -> string -> Document_ID.command -> Command.exec option
     1.8    val remove_versions: Document_ID.version list -> state -> state
     1.9    val start_execution: state -> state
    1.10    val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
    1.11 @@ -406,6 +407,12 @@
    1.12  
    1.13  val the_command_name = #1 oo the_command;
    1.14  
    1.15 +fun command_exec state node_name command_id =
    1.16 +  let
    1.17 +    val State {execution = {version_id, ...}, ...} = state;
    1.18 +    val node = get_node (nodes_of (the_version state version_id)) node_name;
    1.19 +  in the_entry node command_id end;
    1.20 +
    1.21  end;
    1.22  
    1.23  
     2.1 --- a/src/Pure/Tools/debugger.ML	Mon Aug 10 19:17:49 2015 +0200
     2.2 +++ b/src/Pure/Tools/debugger.ML	Mon Aug 10 20:22:49 2015 +0200
     2.3 @@ -234,12 +234,29 @@
     2.4  
     2.5  val _ =
     2.6    Isabelle_Process.protocol_command "Debugger.breakpoint"
     2.7 -    (fn [serial_string, b_string] =>
     2.8 +    (fn [node_name, id0, breakpoint0, breakpoint_state0] =>
     2.9        let
    2.10 -        val serial = Markup.parse_int serial_string;
    2.11 -        val b = Markup.parse_bool b_string;
    2.12 -        (* FIXME *)
    2.13 -      in () end);
    2.14 +        val id = Markup.parse_int id0;
    2.15 +        val breakpoint = Markup.parse_int breakpoint0;
    2.16 +        val breakpoint_state = Markup.parse_bool breakpoint_state0;
    2.17 +
    2.18 +        fun err () = error ("Bad exec for command " ^ Markup.print_int id);
    2.19 +      in
    2.20 +        (case Document.command_exec (Document.state ()) node_name id of
    2.21 +          SOME (eval, _) =>
    2.22 +            if Command.eval_finished eval then
    2.23 +              let
    2.24 +                val st = Command.eval_result_state eval;
    2.25 +                val ctxt = Toplevel.presentation_context_of st
    2.26 +                  handle Toplevel.UNDEF => err ();
    2.27 +              in
    2.28 +                (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of
    2.29 +                  SOME (b, _) => b := breakpoint_state
    2.30 +                | NONE => err ())
    2.31 +              end
    2.32 +            else err ()
    2.33 +        | NONE => err ())
    2.34 +      end);
    2.35  
    2.36  val _ =
    2.37    Isabelle_Process.protocol_command "Debugger.cancel"
     3.1 --- a/src/Pure/Tools/debugger.scala	Mon Aug 10 19:17:49 2015 +0200
     3.2 +++ b/src/Pure/Tools/debugger.scala	Mon Aug 10 20:22:49 2015 +0200
     3.3 @@ -29,12 +29,12 @@
     3.4      def inc_active: State = copy(active = active + 1)
     3.5      def dec_active: State = copy(active = active - 1)
     3.6  
     3.7 -    def toggle_breakpoint(serial: Long): (Boolean, State) =
     3.8 +    def toggle_breakpoint(breakpoint: Long): (Boolean, State) =
     3.9      {
    3.10        val active_breakpoints1 =
    3.11 -        if (active_breakpoints(serial)) active_breakpoints - serial
    3.12 -      else active_breakpoints + serial
    3.13 -      (active_breakpoints1(serial), copy(active_breakpoints = active_breakpoints1))
    3.14 +        if (active_breakpoints(breakpoint)) active_breakpoints - breakpoint
    3.15 +      else active_breakpoints + breakpoint
    3.16 +      (active_breakpoints1(breakpoint), copy(active_breakpoints = active_breakpoints1))
    3.17      }
    3.18  
    3.19      def set_focus(new_focus: Option[Position.T]): State =
    3.20 @@ -141,19 +141,23 @@
    3.21    def inc_active(): Unit = global_state.change(_.inc_active)
    3.22    def dec_active(): Unit = global_state.change(_.dec_active)
    3.23  
    3.24 -  def breakpoint_active(serial: Long): Option[Boolean] =
    3.25 +  def breakpoint_active(breakpoint: Long): Option[Boolean] =
    3.26    {
    3.27      val state = current_state()
    3.28 -    if (state.active > 0) Some(state.active_breakpoints(serial)) else None
    3.29 +    if (state.active > 0) Some(state.active_breakpoints(breakpoint)) else None
    3.30    }
    3.31  
    3.32 -  def toggle_breakpoint(serial: Long)
    3.33 +  def toggle_breakpoint(command: Command, breakpoint: Long)
    3.34    {
    3.35      global_state.change(state =>
    3.36      {
    3.37 -      val (b, state1) = state.toggle_breakpoint(serial)
    3.38 +      val (breakpoint_state, state1) = state.toggle_breakpoint(breakpoint)
    3.39        state1.session.protocol_command(
    3.40 -        "Debugger.breakpoint", Properties.Value.Long(serial), Properties.Value.Boolean(b))
    3.41 +        "Debugger.breakpoint",
    3.42 +        Symbol.encode(command.node_name.node),
    3.43 +        Document_ID(command.id),
    3.44 +        Properties.Value.Long(breakpoint),
    3.45 +        Properties.Value.Boolean(breakpoint_state))
    3.46        state1
    3.47      })
    3.48    }
     4.1 --- a/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 19:17:49 2015 +0200
     4.2 +++ b/src/Tools/jEdit/src/debugger_dockable.scala	Mon Aug 10 20:22:49 2015 +0200
     4.3 @@ -41,15 +41,15 @@
     4.4  
     4.5    /* breakpoints */
     4.6  
     4.7 -  def toggle_breakpoint(serial: Long)
     4.8 +  def toggle_breakpoint(command: Command, breakpoint: Long)
     4.9    {
    4.10      GUI_Thread.require {}
    4.11  
    4.12 -    Debugger.toggle_breakpoint(serial)
    4.13 +    Debugger.toggle_breakpoint(command, breakpoint)
    4.14      jEdit.propertiesChanged()
    4.15    }
    4.16  
    4.17 -  def get_breakpoint(text_area: JEditTextArea, offset: Text.Offset): Option[Long] =
    4.18 +  def get_breakpoint(text_area: JEditTextArea, offset: Text.Offset): Option[(Command, Long)] =
    4.19    {
    4.20      GUI_Thread.require {}
    4.21  
    4.22 @@ -57,7 +57,7 @@
    4.23        case Some(doc_view) =>
    4.24          val rendering = doc_view.get_rendering()
    4.25          val range = JEdit_Lib.point_range(text_area.getBuffer, offset)
    4.26 -        rendering.breakpoints(range).headOption
    4.27 +        rendering.breakpoint(range)
    4.28        case None => None
    4.29      }
    4.30    }
     5.1 --- a/src/Tools/jEdit/src/isabelle.scala	Mon Aug 10 19:17:49 2015 +0200
     5.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Mon Aug 10 20:22:49 2015 +0200
     5.3 @@ -350,8 +350,9 @@
     5.4  
     5.5    def toggle_breakpoint(text_area: JEditTextArea)
     5.6    {
     5.7 -    for (breakpoint <- Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition))
     5.8 -      Debugger_Dockable.toggle_breakpoint(breakpoint)
     5.9 +    for {
    5.10 +      (command, serial) <- Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition)
    5.11 +    } Debugger_Dockable.toggle_breakpoint(command, serial)
    5.12    }
    5.13  
    5.14  
     6.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 19:17:49 2015 +0200
     6.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Aug 10 20:22:49 2015 +0200
     6.3 @@ -343,13 +343,18 @@
     6.4  
     6.5    /* breakpoints */
     6.6  
     6.7 -  def breakpoints(range: Text.Range): List[Long] =
     6.8 -    snapshot.select(range, Rendering.breakpoint_elements, _ =>
     6.9 -      {
    6.10 -        case Text.Info(_, XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(serial)), _)) =>
    6.11 -          Some(serial)
    6.12 -        case _ => None
    6.13 -      }).map(_.info)
    6.14 +  def breakpoint(range: Text.Range): Option[(Command, Long)] =
    6.15 +    if (snapshot.is_outdated) None
    6.16 +    else
    6.17 +      snapshot.select(range, Rendering.breakpoint_elements, command_states =>
    6.18 +        {
    6.19 +          case Text.Info(_, XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(serial)), _)) =>
    6.20 +            command_states match {
    6.21 +              case st :: _ => Some((st.command, serial))
    6.22 +              case _ => None
    6.23 +            }
    6.24 +          case _ => None
    6.25 +        }).headOption.map(_.info)
    6.26  
    6.27  
    6.28    /* command status overview */