src/Pure/Tools/debugger.scala
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (21 months ago)
changeset 67003 49850a679c2c
parent 65344 b99283eed13c
permissions -rw-r--r--
more robust sorted_entries;
     1 /*  Title:      Pure/Tools/debugger.scala
     2     Author:     Makarius
     3 
     4 Interactive debugger for Isabelle/ML.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.collection.immutable.SortedMap
    11 
    12 
    13 object Debugger
    14 {
    15   /* thread context */
    16 
    17   case object Update
    18 
    19   sealed case class Debug_State(pos: Position.T, function: String)
    20   type Threads = SortedMap[String, List[Debug_State]]
    21 
    22   sealed case class Context(thread_name: String, debug_states: List[Debug_State], index: Int = 0)
    23   {
    24     def size: Int = debug_states.length + 1
    25     def reset: Context = copy(index = 0)
    26     def select(i: Int) = copy(index = i + 1)
    27 
    28     def thread_state: Option[Debug_State] = debug_states.headOption
    29 
    30     def stack_state: Option[Debug_State] =
    31       if (1 <= index && index <= debug_states.length)
    32         Some(debug_states(index - 1))
    33       else None
    34 
    35     def debug_index: Option[Int] =
    36       if (stack_state.isDefined) Some(index - 1)
    37       else if (debug_states.nonEmpty) Some(0)
    38       else None
    39 
    40     def debug_state: Option[Debug_State] = stack_state orElse thread_state
    41     def debug_position: Option[Position.T] = debug_state.map(_.pos)
    42 
    43     override def toString: String =
    44       stack_state match {
    45         case None => thread_name
    46         case Some(d) => d.function
    47       }
    48   }
    49 
    50 
    51   /* debugger state */
    52 
    53   sealed case class State(
    54     active: Int = 0,  // active views
    55     break: Boolean = false,  // break at next possible breakpoint
    56     active_breakpoints: Set[Long] = Set.empty,  // explicit breakpoint state
    57     threads: Threads = SortedMap.empty,  // thread name ~> stack of debug states
    58     focus: Map[String, Context] = Map.empty,  // thread name ~> focus
    59     output: Map[String, Command.Results] = Map.empty)  // thread name ~> output messages
    60   {
    61     def set_break(b: Boolean): State = copy(break = b)
    62 
    63     def is_active: Boolean = active > 0
    64     def inc_active: State = copy(active = active + 1)
    65     def dec_active: State = copy(active = active - 1)
    66 
    67     def toggle_breakpoint(breakpoint: Long): (Boolean, State) =
    68     {
    69       val active_breakpoints1 =
    70         if (active_breakpoints(breakpoint)) active_breakpoints - breakpoint
    71       else active_breakpoints + breakpoint
    72       (active_breakpoints1(breakpoint), copy(active_breakpoints = active_breakpoints1))
    73     }
    74 
    75     def get_thread(thread_name: String): List[Debug_State] =
    76       threads.getOrElse(thread_name, Nil)
    77 
    78     def update_thread(thread_name: String, debug_states: List[Debug_State]): State =
    79     {
    80       val threads1 =
    81         if (debug_states.nonEmpty) threads + (thread_name -> debug_states)
    82         else threads - thread_name
    83       val focus1 =
    84         focus.get(thread_name) match {
    85           case Some(c) if debug_states.nonEmpty =>
    86             focus + (thread_name -> Context(thread_name, debug_states))
    87           case _ => focus - thread_name
    88         }
    89       copy(threads = threads1, focus = focus1)
    90     }
    91 
    92     def set_focus(c: Context): State = copy(focus = focus + (c.thread_name -> c))
    93 
    94     def get_output(thread_name: String): Command.Results =
    95       output.getOrElse(thread_name, Command.Results.empty)
    96 
    97     def add_output(thread_name: String, entry: Command.Results.Entry): State =
    98       copy(output = output + (thread_name -> (get_output(thread_name) + entry)))
    99 
   100     def clear_output(thread_name: String): State =
   101       copy(output = output - thread_name)
   102   }
   103 
   104 
   105   /* protocol handler */
   106 
   107   class Handler(session: Session) extends Session.Protocol_Handler
   108   {
   109     val debugger: Debugger = new Debugger(session)
   110 
   111     private def debugger_state(msg: Prover.Protocol_Output): Boolean =
   112     {
   113       msg.properties match {
   114         case Markup.Debugger_State(thread_name) =>
   115           val msg_body = Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes))
   116           val debug_states =
   117           {
   118             import XML.Decode._
   119             list(pair(properties, string))(msg_body).map({
   120               case (pos, function) => Debug_State(pos, function)
   121             })
   122           }
   123           debugger.update_thread(thread_name, debug_states)
   124           true
   125         case _ => false
   126       }
   127     }
   128 
   129     private def debugger_output(msg: Prover.Protocol_Output): Boolean =
   130     {
   131       msg.properties match {
   132         case Markup.Debugger_Output(thread_name) =>
   133           Symbol.decode_yxml_failsafe(UTF8.decode_permissive(msg.bytes)) match {
   134             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
   135               val message = XML.Elem(Markup(Markup.message(name), props), body)
   136               debugger.add_output(thread_name, i -> session.xml_cache.elem(message))
   137               true
   138             case _ => false
   139           }
   140         case _ => false
   141       }
   142     }
   143 
   144     val functions =
   145       List(
   146         Markup.DEBUGGER_STATE -> debugger_state _,
   147         Markup.DEBUGGER_OUTPUT -> debugger_output _)
   148   }
   149 }
   150 
   151 class Debugger private(session: Session)
   152 {
   153   /* debugger state */
   154 
   155   private val state = Synchronized(Debugger.State())
   156 
   157   private val delay_update =
   158     Standard_Thread.delay_first(session.output_delay) {
   159       session.debugger_updates.post(Debugger.Update)
   160     }
   161 
   162 
   163   /* protocol commands */
   164 
   165   def update_thread(thread_name: String, debug_states: List[Debugger.Debug_State])
   166   {
   167     state.change(_.update_thread(thread_name, debug_states))
   168     delay_update.invoke()
   169   }
   170 
   171   def add_output(thread_name: String, entry: Command.Results.Entry)
   172   {
   173     state.change(_.add_output(thread_name, entry))
   174     delay_update.invoke()
   175   }
   176 
   177   def is_active(): Boolean = session.is_ready && state.value.is_active
   178 
   179   def ready()
   180   {
   181     if (is_active())
   182       session.protocol_command("Debugger.init")
   183   }
   184 
   185   def init(): Unit =
   186     state.change(st =>
   187     {
   188       val st1 = st.inc_active
   189       if (session.is_ready && !st.is_active && st1.is_active)
   190         session.protocol_command("Debugger.init")
   191       st1
   192     })
   193 
   194   def exit(): Unit =
   195     state.change(st =>
   196     {
   197       val st1 = st.dec_active
   198       if (session.is_ready && st.is_active && !st1.is_active)
   199         session.protocol_command("Debugger.exit")
   200       st1
   201     })
   202 
   203   def is_break(): Boolean = state.value.break
   204   def set_break(b: Boolean)
   205   {
   206     state.change(st => {
   207       val st1 = st.set_break(b)
   208       session.protocol_command("Debugger.break", b.toString)
   209       st1
   210     })
   211     delay_update.invoke()
   212   }
   213 
   214   def active_breakpoint_state(breakpoint: Long): Option[Boolean] =
   215   {
   216     val st = state.value
   217     if (st.is_active) Some(st.active_breakpoints(breakpoint)) else None
   218   }
   219 
   220   def breakpoint_state(breakpoint: Long): Boolean =
   221     state.value.active_breakpoints(breakpoint)
   222 
   223   def toggle_breakpoint(command: Command, breakpoint: Long)
   224   {
   225     state.change(st =>
   226       {
   227         val (breakpoint_state, st1) = st.toggle_breakpoint(breakpoint)
   228         session.protocol_command(
   229           "Debugger.breakpoint",
   230           Symbol.encode(command.node_name.node),
   231           Document_ID(command.id),
   232           Value.Long(breakpoint),
   233           Value.Boolean(breakpoint_state))
   234         st1
   235       })
   236   }
   237 
   238   def status(focus: Option[Debugger.Context]): (Debugger.Threads, List[XML.Tree]) =
   239   {
   240     val st = state.value
   241     val output =
   242       focus match {
   243         case None => Nil
   244         case Some(c) =>
   245           (for {
   246             (thread_name, results) <- st.output
   247             if thread_name == c.thread_name
   248             (_, tree) <- results.iterator
   249           } yield tree).toList
   250       }
   251     (st.threads, output)
   252   }
   253 
   254   def focus(): List[Debugger.Context] = state.value.focus.toList.map(_._2)
   255   def set_focus(c: Debugger.Context)
   256   {
   257     state.change(_.set_focus(c))
   258     delay_update.invoke()
   259   }
   260 
   261   def input(thread_name: String, msg: String*): Unit =
   262     session.protocol_command("Debugger.input", (thread_name :: msg.toList):_*)
   263 
   264   def continue(thread_name: String): Unit = input(thread_name, "continue")
   265   def step(thread_name: String): Unit = input(thread_name, "step")
   266   def step_over(thread_name: String): Unit = input(thread_name, "step_over")
   267   def step_out(thread_name: String): Unit = input(thread_name, "step_out")
   268 
   269   def clear_output(thread_name: String)
   270   {
   271     state.change(_.clear_output(thread_name))
   272     delay_update.invoke()
   273   }
   274 
   275   def eval(c: Debugger.Context, SML: Boolean, context: String, expression: String)
   276   {
   277     state.change(st => {
   278       input(c.thread_name, "eval", c.debug_index.getOrElse(0).toString,
   279         SML.toString, Symbol.encode(context), Symbol.encode(expression))
   280       st.clear_output(c.thread_name)
   281     })
   282     delay_update.invoke()
   283   }
   284 
   285   def print_vals(c: Debugger.Context, SML: Boolean, context: String)
   286   {
   287     require(c.debug_index.isDefined)
   288 
   289     state.change(st => {
   290       input(c.thread_name, "print_vals", c.debug_index.getOrElse(0).toString,
   291         SML.toString, Symbol.encode(context))
   292       st.clear_output(c.thread_name)
   293     })
   294     delay_update.invoke()
   295   }
   296 }