interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
authorLars Hupel <lars.hupel@mytum.de>
Tue Feb 04 09:04:59 2014 +0000 (2014-02-04)
changeset 55316885500f4aa6a
parent 55315 54b0352fb46d
child 55317 834a84553e02
interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
CONTRIBUTORS
NEWS
src/Pure/PIDE/markup.scala
src/Pure/System/session.scala
src/Pure/Tools/simplifier_trace.ML
src/Pure/Tools/simplifier_trace.scala
src/Pure/raw_simplifier.ML
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/dockables.xml
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jEdit.props
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/simplifier_trace_dockable.scala
src/Tools/jEdit/src/simplifier_trace_window.scala
     1.1 --- a/CONTRIBUTORS	Tue Feb 04 01:35:48 2014 +0100
     1.2 +++ b/CONTRIBUTORS	Tue Feb 04 09:04:59 2014 +0000
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* January 2014: Lars Hupel, TUM
     1.8 +  An improved, interactive simplifier trace with integration into the
     1.9 +  Isabelle/jEdit Prover IDE.
    1.10  
    1.11  Contributions to Isabelle2013-1
    1.12  -------------------------------
     2.1 --- a/NEWS	Tue Feb 04 01:35:48 2014 +0100
     2.2 +++ b/NEWS	Tue Feb 04 09:04:59 2014 +0000
     2.3 @@ -37,6 +37,10 @@
     2.4  process, without requiring old-fashioned command-line invocation of
     2.5  "isabelle jedit -m MODE".
     2.6  
     2.7 +* New panel: Simplifier trace.  Provides an interactive view of the
     2.8 +simplification process, enabled by the newly-introduced
     2.9 +"simplifier_trace" declaration.
    2.10 +
    2.11  
    2.12  *** Pure ***
    2.13  
     3.1 --- a/src/Pure/PIDE/markup.scala	Tue Feb 04 01:35:48 2014 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Tue Feb 04 09:04:59 2014 +0000
     3.3 @@ -273,7 +273,8 @@
     3.4  
     3.5    /* messages */
     3.6  
     3.7 -  val Serial = new Properties.Long("serial")
     3.8 +  val SERIAL = "serial"
     3.9 +  val Serial = new Properties.Long(SERIAL)
    3.10  
    3.11    val MESSAGE = "message"
    3.12  
    3.13 @@ -386,6 +387,76 @@
    3.14          case _ => None
    3.15        }
    3.16    }
    3.17 +
    3.18 +  /* simplifier trace */
    3.19 +
    3.20 +  val TEXT = "text"
    3.21 +  val Text = new Properties.String(TEXT)
    3.22 +
    3.23 +  val PARENT = "parent"
    3.24 +  val Parent = new Properties.Long(PARENT)
    3.25 +
    3.26 +  val SUCCESS = "success"
    3.27 +  val Success = new Properties.Boolean(SUCCESS)
    3.28 +
    3.29 +  val CANCEL_SIMP_TRACE = "simp_trace_cancel"
    3.30 +  object Cancel_Simp_Trace
    3.31 +  {
    3.32 +    def unapply(props: Properties.T): Option[Long] =
    3.33 +      props match {
    3.34 +        case (FUNCTION, CANCEL_SIMP_TRACE) :: Serial(id) => Some(id)
    3.35 +        case _ => None
    3.36 +      }
    3.37 +  }
    3.38 +
    3.39 +  val SIMP_TRACE = "simp_trace"
    3.40 +  object Simp_Trace
    3.41 +  {
    3.42 +    def unapply(tree: XML.Tree): Option[(Long, Simplifier_Trace.Answer)] =
    3.43 +      tree match {
    3.44 +        case XML.Elem(Markup(SIMP_TRACE, props), _) =>
    3.45 +          (props, props) match {
    3.46 +            case (Serial(serial), Name(name)) =>
    3.47 +              Simplifier_Trace.all_answers.find(_.name == name).map((serial, _))
    3.48 +            case _ =>
    3.49 +              None
    3.50 +          }
    3.51 +        case _ =>
    3.52 +          None
    3.53 +      }
    3.54 +  }
    3.55 +
    3.56 +  /* trace items from the prover */
    3.57 +
    3.58 +  object Simp_Trace_Item
    3.59 +  {
    3.60 +
    3.61 +    def unapply(tree: XML.Tree): Option[(String, Data)] =
    3.62 +      tree match {
    3.63 +        case XML.Elem(Markup(RESULT, Serial(serial)), List(
    3.64 +          XML.Elem(Markup(markup, props), content)
    3.65 +        )) if markup.startsWith("simp_trace_") =>
    3.66 +          (props, props) match {
    3.67 +            case (Text(text), Parent(parent)) =>
    3.68 +              Some((markup, Data(serial, markup, text, parent, props, content)))
    3.69 +            case _ =>
    3.70 +              None
    3.71 +          }
    3.72 +        case _ =>
    3.73 +          None
    3.74 +      }
    3.75 +
    3.76 +    val LOG = "simp_trace_log"
    3.77 +    val STEP = "simp_trace_step"
    3.78 +    val RECURSE = "simp_trace_recurse"
    3.79 +    val HINT = "simp_trace_hint"
    3.80 +    val IGNORE = "simp_trace_ignore"
    3.81 +
    3.82 +    case class Data(serial: Long, markup: String, text: String,
    3.83 +                    parent: Long, props: Properties.T, content: XML.Body)
    3.84 +
    3.85 +  }
    3.86 +
    3.87  }
    3.88  
    3.89  
     4.1 --- a/src/Pure/System/session.scala	Tue Feb 04 01:35:48 2014 +0100
     4.2 +++ b/src/Pure/System/session.scala	Tue Feb 04 09:04:59 2014 +0000
     4.3 @@ -139,7 +139,7 @@
     4.4    val syslog_messages = new Event_Bus[Isabelle_Process.Output]
     4.5    val raw_output_messages = new Event_Bus[Isabelle_Process.Output]
     4.6    val all_messages = new Event_Bus[Isabelle_Process.Message]  // potential bottle-neck
     4.7 -
     4.8 +  val trace_events = new Event_Bus[Simplifier_Trace.Event.type]
     4.9  
    4.10  
    4.11    /** buffered command changes (delay_first discipline) **/
     5.1 --- a/src/Pure/Tools/simplifier_trace.ML	Tue Feb 04 01:35:48 2014 +0100
     5.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Tue Feb 04 09:04:59 2014 +0000
     5.3 @@ -1,38 +1,435 @@
     5.4  (*  Title:      Pure/Tools/simplifier_trace.ML
     5.5 -    Author:     Lars Hupel, TU Muenchen
     5.6 +    Author:     Lars Hupel
     5.7  
     5.8  Interactive Simplifier trace.
     5.9  *)
    5.10  
    5.11  signature SIMPLIFIER_TRACE =
    5.12  sig
    5.13 -  val simp_trace_test: bool Config.T
    5.14 +  val add_term_breakpoint: term -> Context.generic -> Context.generic
    5.15 +  val add_thm_breakpoint: thm -> Context.generic -> Context.generic
    5.16  end
    5.17  
    5.18  structure Simplifier_Trace: SIMPLIFIER_TRACE =
    5.19  struct
    5.20  
    5.21 -(* Simplifier trace operations *)
    5.22 +(** background data **)
    5.23 +
    5.24 +datatype mode = Disabled | Normal | Full
    5.25 +
    5.26 +fun merge_modes Disabled m = m
    5.27 +  | merge_modes Normal Full = Full
    5.28 +  | merge_modes Normal _ = Normal
    5.29 +  | merge_modes Full _ = Full
    5.30 +
    5.31 +val empty_breakpoints =
    5.32 +  (Item_Net.init (op =) single (* FIXME equality on terms? *),
    5.33 +   Item_Net.init eq_rrule (single o Thm.full_prop_of o #thm))
    5.34 +
    5.35 +fun merge_breakpoints ((term_bs1, thm_bs1), (term_bs2, thm_bs2)) =
    5.36 +  (Item_Net.merge (term_bs1, term_bs2),
    5.37 +   Item_Net.merge (thm_bs1, thm_bs2))
    5.38 +
    5.39 +structure Data = Generic_Data
    5.40 +(
    5.41 +  type T =
    5.42 +    {max_depth: int,
    5.43 +     depth: int,
    5.44 +     mode: mode,
    5.45 +     interactive: bool,
    5.46 +     parent: int,
    5.47 +     breakpoints: term Item_Net.T * rrule Item_Net.T}
    5.48 +  val empty =
    5.49 +    {max_depth = 10,
    5.50 +     depth = 0,
    5.51 +     mode = Disabled,
    5.52 +     interactive = false,
    5.53 +     parent = 0,
    5.54 +     breakpoints = empty_breakpoints}
    5.55 +  val extend = I
    5.56 +  fun merge ({max_depth = max_depth1, mode = mode1, interactive = interactive1,
    5.57 +              breakpoints = breakpoints1, ...},
    5.58 +             {max_depth = max_depth2, mode = mode2, interactive = interactive2,
    5.59 +              breakpoints = breakpoints2, ...}) =
    5.60 +    {max_depth = Int.max (max_depth1, max_depth2),
    5.61 +     depth = 0,
    5.62 +     mode = merge_modes mode1 mode2,
    5.63 +     interactive = interactive1 orelse interactive2,
    5.64 +     parent = 0,
    5.65 +     breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}
    5.66 +)
    5.67 +
    5.68 +fun map_breakpoints f_term f_thm =
    5.69 +  Data.map (fn {max_depth, depth, mode, interactive, parent, breakpoints = (term_bs, thm_bs)} =>
    5.70 +    {max_depth = max_depth,
    5.71 +     depth = depth,
    5.72 +     mode = mode,
    5.73 +     interactive = interactive,
    5.74 +     parent = parent,
    5.75 +     breakpoints = (f_term term_bs, f_thm thm_bs)})
    5.76 +
    5.77 +fun add_term_breakpoint term =
    5.78 +  map_breakpoints (Item_Net.update term) I
    5.79 +
    5.80 +fun add_thm_breakpoint thm context =
    5.81 +  let
    5.82 +    val rrules = mk_rrules (Context.proof_of context) [thm]
    5.83 +  in
    5.84 +    map_breakpoints I (fold Item_Net.update rrules) context
    5.85 +  end
    5.86 +
    5.87 +fun is_breakpoint (term, rrule) context =
    5.88 +  let
    5.89 +    val {breakpoints, ...} = Data.get context
    5.90 +
    5.91 +    fun matches pattern = Pattern.matches (Context.theory_of context) (pattern, term)
    5.92 +    val term_matches = filter matches (Item_Net.retrieve_matching (fst breakpoints) term)
    5.93 +
    5.94 +    val {thm = thm, ...} = rrule
    5.95 +    val thm_matches = exists (eq_rrule o pair rrule)
    5.96 +      (Item_Net.retrieve_matching (snd breakpoints) (Thm.full_prop_of thm))
    5.97 +  in
    5.98 +    (term_matches, thm_matches)
    5.99 +  end
   5.100 +
   5.101 +(** config and attributes **)
   5.102 +
   5.103 +fun config raw_mode interactive max_depth =
   5.104 +  let
   5.105 +    val mode = case raw_mode of
   5.106 +      "normal" => Normal
   5.107 +    | "full" => Full
   5.108 +    | _ => error ("Simplifier_Trace.config: unknown mode " ^ raw_mode)
   5.109 +
   5.110 +    val update = Data.map (fn {depth, parent, breakpoints, ...} =>
   5.111 +      {max_depth = max_depth,
   5.112 +       depth = depth,
   5.113 +       mode = mode,
   5.114 +       interactive = interactive,
   5.115 +       parent = parent,
   5.116 +       breakpoints = breakpoints})
   5.117 +  in Thm.declaration_attribute (K update) end
   5.118 +
   5.119 +fun term_breakpoint terms =
   5.120 +  Thm.declaration_attribute (K (fold add_term_breakpoint terms))
   5.121 +
   5.122 +val thm_breakpoint =
   5.123 +  Thm.declaration_attribute add_thm_breakpoint
   5.124 +
   5.125 +(** tracing state **)
   5.126 +
   5.127 +val futures =
   5.128 +  Synchronized.var "Simplifier_Trace.futures" (Inttab.empty: string future Inttab.table)
   5.129 +
   5.130 +(** markup **)
   5.131 +
   5.132 +fun output_result (id, data) =
   5.133 +  Output.result (Markup.serial_properties id) data
   5.134 +
   5.135 +val serialN = "serial"
   5.136 +val parentN = "parent"
   5.137 +val textN = "text"
   5.138 +val successN = "success"
   5.139 +
   5.140 +val logN = "simp_trace_log"
   5.141 +val stepN = "simp_trace_step"
   5.142 +val recurseN = "simp_trace_recurse"
   5.143 +val hintN = "simp_trace_hint"
   5.144 +val ignoreN = "simp_trace_ignore"
   5.145 +
   5.146 +val cancelN = "simp_trace_cancel"
   5.147 +
   5.148 +type payload =
   5.149 +  {props: Properties.T,
   5.150 +   pretty: Pretty.T}
   5.151 +
   5.152 +fun empty_payload () : payload =
   5.153 +  {props = [], pretty = Pretty.str ""}
   5.154 +
   5.155 +fun mk_generic_result markup text triggered (payload : unit -> payload) ctxt =
   5.156 +  let
   5.157 +    val {max_depth, depth, mode, interactive, parent, ...} = Data.get (Context.Proof ctxt)
   5.158 +
   5.159 +    val eligible =
   5.160 +      case mode of
   5.161 +        Disabled => false
   5.162 +      | Normal => triggered
   5.163 +      | Full => true
   5.164 +
   5.165 +    val markup' = if markup = stepN andalso not interactive then logN else markup
   5.166 +  in
   5.167 +    if not eligible orelse depth > max_depth then
   5.168 +      NONE
   5.169 +    else
   5.170 +      let
   5.171 +        val {props = more_props, pretty} = payload ()
   5.172 +        val props =
   5.173 +          [(textN, text),
   5.174 +           (parentN, Markup.print_int parent)]
   5.175 +        val data =
   5.176 +          Pretty.string_of (Pretty.markup (markup', props @ more_props) [pretty])
   5.177 +      in
   5.178 +        SOME (serial (), data)
   5.179 +      end
   5.180 +  end
   5.181 +
   5.182 +(** tracing output **)
   5.183 +
   5.184 +fun send_request (result_id, content) =
   5.185 +  let
   5.186 +    fun break () =
   5.187 +      (Output.protocol_message
   5.188 +         [(Markup.functionN, cancelN),
   5.189 +          (serialN, Markup.print_int result_id)]
   5.190 +         "";
   5.191 +       Synchronized.change futures (Inttab.delete_safe result_id))
   5.192 +    val promise = Future.promise break : string future
   5.193 +  in
   5.194 +    Synchronized.change futures (Inttab.update_new (result_id, promise));
   5.195 +    output_result (result_id, content);
   5.196 +    promise
   5.197 +  end
   5.198 +
   5.199 +
   5.200 +fun step {term, thm, unconditional, ctxt, rrule} =
   5.201 +  let
   5.202 +    val (matching_terms, thm_triggered) = is_breakpoint (term, rrule) (Context.Proof ctxt)
   5.203 +
   5.204 +    val {name, ...} = rrule
   5.205 +    val term_triggered = not (null matching_terms)
   5.206  
   5.207 -val simp_trace_test =
   5.208 -  Attrib.setup_config_bool @{binding simp_trace_test} (K false)
   5.209 +    val text =
   5.210 +      if unconditional then
   5.211 +        "Apply rewrite rule?"
   5.212 +      else
   5.213 +        "Apply conditional rewrite rule?"
   5.214 +
   5.215 +    fun payload () =
   5.216 +      let
   5.217 +        (* FIXME pretty printing via Proof_Context.pretty_fact *)
   5.218 +        val pretty_thm = Pretty.block
   5.219 +          [Pretty.str ("Instance of " ^ name ^ ":"),
   5.220 +           Pretty.brk 1,
   5.221 +           Syntax.pretty_term ctxt (Thm.prop_of thm)]
   5.222 +
   5.223 +        val pretty_term = Pretty.block
   5.224 +          [Pretty.str "Trying to rewrite:",
   5.225 +           Pretty.brk 1,
   5.226 +           Syntax.pretty_term ctxt term]
   5.227 +
   5.228 +        val pretty_matchings =
   5.229 +          let
   5.230 +            val items = map (Pretty.item o single o Syntax.pretty_term ctxt) matching_terms
   5.231 +          in
   5.232 +            if not (null matching_terms) then
   5.233 +              [Pretty.block (Pretty.fbreaks (Pretty.str "Matching terms:" :: items))]
   5.234 +            else
   5.235 +              []
   5.236 +          end
   5.237 +
   5.238 +        val pretty =
   5.239 +          Pretty.chunks ([pretty_thm, pretty_term] @ pretty_matchings)
   5.240 +      in
   5.241 +        {props = [], pretty = pretty}
   5.242 +      end
   5.243 +
   5.244 +    val {max_depth, depth, mode, interactive, breakpoints, ...} =
   5.245 +      Data.get (Context.Proof ctxt)
   5.246 +
   5.247 +    fun mk_promise result =
   5.248 +      let
   5.249 +        val result_id = #1 result
   5.250 +
   5.251 +        fun put mode' interactive' = Data.put
   5.252 +          {max_depth = max_depth,
   5.253 +           depth = depth,
   5.254 +           mode = mode',
   5.255 +           interactive = interactive',
   5.256 +           parent = result_id,
   5.257 +           breakpoints = breakpoints} (Context.Proof ctxt) |>
   5.258 +          Context.the_proof
   5.259 +
   5.260 +        fun to_response "skip" = NONE
   5.261 +          | to_response "continue" = SOME (put mode true)
   5.262 +          | to_response "continue_trace" = SOME (put Full true)
   5.263 +          | to_response "continue_passive" = SOME (put mode false)
   5.264 +          | to_response "continue_disable" = SOME (put Disabled false)
   5.265 +          | to_response _ = raise Fail "Simplifier_Trace.step: invalid message"
   5.266 +      in
   5.267 +        if not interactive then
   5.268 +          (output_result result; Future.value (SOME (put mode false)))
   5.269 +        else
   5.270 +          Future.map to_response (send_request result)
   5.271 +      end
   5.272 +
   5.273 +  in
   5.274 +    case mk_generic_result stepN text (thm_triggered orelse term_triggered) payload ctxt of
   5.275 +      NONE => Future.value (SOME ctxt)
   5.276 +    | SOME res => mk_promise res
   5.277 +  end
   5.278 +
   5.279 +fun recurse text term ctxt =
   5.280 +  let
   5.281 +    fun payload () =
   5.282 +      {props = [],
   5.283 +       pretty = Syntax.pretty_term ctxt term}
   5.284 +
   5.285 +    val {max_depth, depth, mode, interactive, breakpoints, ...} = Data.get (Context.Proof ctxt)
   5.286 +
   5.287 +    fun put result_id = Data.put
   5.288 +      {max_depth = max_depth,
   5.289 +       depth = depth + 1,
   5.290 +       mode = if depth >= max_depth then Disabled else mode,
   5.291 +       interactive = interactive,
   5.292 +       parent = result_id,
   5.293 +       breakpoints = breakpoints} (Context.Proof ctxt)
   5.294 +
   5.295 +    val context' =
   5.296 +      case mk_generic_result recurseN text true payload ctxt of
   5.297 +        NONE =>
   5.298 +          put 0
   5.299 +      | SOME res =>
   5.300 +          (output_result res; put (#1 res))
   5.301 +  in Context.the_proof context' end
   5.302 +
   5.303 +fun indicate_failure {term, ctxt, thm, rrule, ...} ctxt' =
   5.304 +  let
   5.305 +    fun payload () =
   5.306 +      let
   5.307 +        val {name, ...} = rrule
   5.308 +        val pretty_thm =
   5.309 +          (* FIXME pretty printing via Proof_Context.pretty_fact *)
   5.310 +          Pretty.block
   5.311 +            [Pretty.str ("In an instance of " ^ name ^ ":"),
   5.312 +             Pretty.brk 1,
   5.313 +             Syntax.pretty_term ctxt (Thm.prop_of thm)]
   5.314 +
   5.315 +        val pretty_term =
   5.316 +          Pretty.block
   5.317 +            [Pretty.str "Was trying to rewrite:",
   5.318 +             Pretty.brk 1,
   5.319 +             Syntax.pretty_term ctxt term]
   5.320 +
   5.321 +        val pretty =
   5.322 +          Pretty.chunks [pretty_thm, pretty_term]
   5.323 +      in
   5.324 +        {props = [(successN, "false")], pretty = pretty}
   5.325 +      end
   5.326 +
   5.327 +    val {interactive, ...} = Data.get (Context.Proof ctxt)
   5.328 +    val {parent, ...} = Data.get (Context.Proof ctxt')
   5.329 +
   5.330 +    fun mk_promise result =
   5.331 +      let
   5.332 +        val result_id = #1 result
   5.333 +
   5.334 +        fun to_response "exit" =
   5.335 +              false
   5.336 +          | to_response "redo" =
   5.337 +              (Option.app output_result
   5.338 +                (mk_generic_result ignoreN "Ignore" true empty_payload ctxt');
   5.339 +               true)
   5.340 +          | to_response _ =
   5.341 +              raise Fail "Simplifier_Trace.indicate_failure: invalid message"
   5.342 +      in
   5.343 +        if not interactive then
   5.344 +          (output_result result; Future.value false)
   5.345 +        else
   5.346 +          Future.map to_response (send_request result)
   5.347 +      end
   5.348 +  in
   5.349 +    case mk_generic_result hintN "Step failed" true payload ctxt' of
   5.350 +      NONE => Future.value false
   5.351 +    | SOME res => mk_promise res
   5.352 +  end
   5.353 +
   5.354 +fun indicate_success thm ctxt =
   5.355 +  let
   5.356 +    fun payload () =
   5.357 +      {props = [(successN, "true")],
   5.358 +       pretty = Syntax.pretty_term ctxt (Thm.prop_of thm)}
   5.359 +  in
   5.360 +    Option.app output_result (mk_generic_result hintN "Successfully rewrote" true payload ctxt)
   5.361 +  end
   5.362 +
   5.363 +(** setup **)
   5.364 +
   5.365 +fun simp_if_continue args ctxt cont =
   5.366 +  let
   5.367 +    val {unconditional: bool, term: term, thm: thm, rrule: rrule} = args
   5.368 +    val data =
   5.369 +      {term = term,
   5.370 +       unconditional = unconditional,
   5.371 +       ctxt = ctxt,
   5.372 +       thm = thm,
   5.373 +       rrule = rrule}
   5.374 +  in
   5.375 +    case Future.join (step data) of
   5.376 +      NONE =>
   5.377 +        NONE
   5.378 +    | SOME ctxt' =>
   5.379 +        let val res = cont ctxt' in
   5.380 +          case res of
   5.381 +            NONE =>
   5.382 +              if Future.join (indicate_failure data ctxt') then
   5.383 +                simp_if_continue args ctxt cont
   5.384 +              else
   5.385 +                NONE
   5.386 +          | SOME (thm, _) =>
   5.387 +              (indicate_success thm ctxt';
   5.388 +               res)
   5.389 +        end
   5.390 +  end
   5.391 +
   5.392 +val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler"
   5.393  
   5.394  val _ = Theory.setup
   5.395    (Simplifier.set_trace_ops
   5.396 -   {trace_invoke = fn {depth, term} => fn ctxt =>
   5.397 -      (if Config.get ctxt simp_trace_test then
   5.398 -        tracing ("Simplifier invocation " ^ string_of_int depth ^ ": " ^
   5.399 -          Syntax.string_of_term ctxt term)
   5.400 -       else (); ctxt),
   5.401 -    trace_apply = fn args => fn ctxt => fn cont =>
   5.402 -      (if Config.get ctxt simp_trace_test then
   5.403 -        tracing ("Simplifier " ^ @{make_string} args)
   5.404 -       else (); cont ctxt)})
   5.405 +    {trace_invoke = fn {depth, term} => recurse "Simplifier invoked" term,
   5.406 +     trace_apply = simp_if_continue})
   5.407 +
   5.408 +val _ =
   5.409 +  Isabelle_Process.protocol_command "Document.simp_trace_reply"
   5.410 +    (fn [s, r] =>
   5.411 +      let
   5.412 +        val serial = Markup.parse_int s
   5.413 +        fun lookup_delete tab =
   5.414 +          (Inttab.lookup tab serial, Inttab.delete_safe serial tab)
   5.415 +        fun apply_result (SOME promise) = Future.fulfill promise r
   5.416 +          | apply_result NONE = () (* FIXME handle protocol failure, just like in active.ML? *)
   5.417 +      in
   5.418 +        (Synchronized.change_result futures lookup_delete |> apply_result)
   5.419 +          handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn
   5.420 +      end)
   5.421 +
   5.422 +(** attributes **)
   5.423 +
   5.424 +val pat_parser =
   5.425 +  Args.context -- Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_schematic
   5.426  
   5.427 +val mode_parser: string parser =
   5.428 +  Scan.optional
   5.429 +    (Args.$$$ "mode" |-- Args.$$$ "=" |-- (Args.$$$ "normal" || Args.$$$ "full"))
   5.430 +    "normal"
   5.431  
   5.432 -(* PIDE protocol *)
   5.433 +val interactive_parser: bool parser =
   5.434 +  Scan.optional (Args.$$$ "interactive" >> K true) false
   5.435 +
   5.436 +val depth_parser =
   5.437 +  Scan.optional (Args.$$$ "depth" |-- Args.$$$ "=" |-- Parse.nat) 10
   5.438 +
   5.439 +val config_parser =
   5.440 +  (interactive_parser -- mode_parser -- depth_parser) >>
   5.441 +    (fn ((interactive, mode), depth) => config mode interactive depth)
   5.442  
   5.443 -val _ = Session.protocol_handler "isabelle.Simplifier_Trace$Handler"
   5.444 +val _ = Theory.setup
   5.445 +  (Attrib.setup @{binding break_term}
   5.446 +    ((Scan.repeat1 pat_parser) >> term_breakpoint)
   5.447 +    "declaration of a term breakpoint" #>
   5.448 +   Attrib.setup @{binding break_thm}
   5.449 +    (Scan.succeed thm_breakpoint)
   5.450 +    "declaration of a theorem breakpoint" #>
   5.451 +   Attrib.setup @{binding simplifier_trace} (Scan.lift config_parser)
   5.452 +    "simplifier trace configuration")
   5.453  
   5.454  end
   5.455 -
     6.1 --- a/src/Pure/Tools/simplifier_trace.scala	Tue Feb 04 01:35:48 2014 +0100
     6.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Tue Feb 04 09:04:59 2014 +0000
     6.3 @@ -1,18 +1,279 @@
     6.4  /*  Title:      Pure/Tools/simplifier_trace.scala
     6.5 -    Author:     Lars Hupel, TU Muenchen
     6.6 +    Author:     Lars Hupel
     6.7  
     6.8  Interactive Simplifier trace.
     6.9  */
    6.10  
    6.11  package isabelle
    6.12  
    6.13 +import scala.actors.Actor._
    6.14 +import scala.annotation.tailrec
    6.15 +import scala.collection.immutable.SortedMap
    6.16 +
    6.17  
    6.18  object Simplifier_Trace
    6.19  {
    6.20 -  /* PIDE protocol */
    6.21 +
    6.22 +  import Markup.Simp_Trace_Item
    6.23 +
    6.24 +
    6.25 +  /* replies to the prover */
    6.26 +
    6.27 +  case class Answer private[Simplifier_Trace](val name: String, val string: String)
    6.28 +
    6.29 +  object Answer
    6.30 +  {
    6.31 +
    6.32 +    object step
    6.33 +    {
    6.34 +      val skip = Answer("skip", "Skip")
    6.35 +      val continue = Answer("continue", "Continue")
    6.36 +      val continue_trace = Answer("continue_trace", "Continue (with full trace)")
    6.37 +      val continue_passive = Answer("continue_passive", "Continue (without asking)")
    6.38 +      val continue_disable = Answer("continue_disable", "Continue (without any trace)")
    6.39 +
    6.40 +      val default = skip
    6.41 +      val all = List(continue, continue_trace, continue_passive, continue_disable, skip)
    6.42 +    }
    6.43 +
    6.44 +    object hint_fail
    6.45 +    {
    6.46 +      val exit = Answer("exit", "Exit")
    6.47 +      val redo = Answer("redo", "Redo")
    6.48 +
    6.49 +      val default = exit
    6.50 +      val all = List(redo, exit)
    6.51 +    }
    6.52 +
    6.53 +  }
    6.54 +
    6.55 +  val all_answers = Answer.step.all ++ Answer.hint_fail.all
    6.56 +
    6.57 +
    6.58 +  /* GUI interaction */
    6.59 +
    6.60 +  case object Event
    6.61 +
    6.62 +
    6.63 +  /* manager actor */
    6.64 +
    6.65 +  private case class Handle_Results(session: Session, id: Document_ID.Command, results: Command.Results)
    6.66 +  private case class Generate_Trace(results: Command.Results)
    6.67 +  private case class Cancel(serial: Long)
    6.68 +  private object Clear_Memory
    6.69 +  private object Stop
    6.70 +  case class Reply(session: Session, serial: Long, answer: Answer)
    6.71 +
    6.72 +  case class Question(data: Simp_Trace_Item.Data, answers: List[Answer], default_answer: Answer)
    6.73 +
    6.74 +  case class Context(
    6.75 +    last_serial: Long = 0L,
    6.76 +    questions: SortedMap[Long, Question] = SortedMap.empty
    6.77 +  )
    6.78 +  {
    6.79 +
    6.80 +    def +(q: Question): Context =
    6.81 +      copy(questions = questions + ((q.data.serial, q)))
    6.82 +
    6.83 +    def -(s: Long): Context =
    6.84 +      copy(questions = questions - s)
    6.85 +
    6.86 +    def with_serial(s: Long): Context =
    6.87 +      copy(last_serial = Math.max(last_serial, s))
    6.88 +
    6.89 +  }
    6.90 +
    6.91 +  case class Trace(entries: List[Simp_Trace_Item.Data])
    6.92 +
    6.93 +  case class Index(text: String, content: XML.Body)
    6.94 +
    6.95 +  object Index
    6.96 +  {
    6.97 +    def of_data(data: Simp_Trace_Item.Data): Index =
    6.98 +      Index(data.text, data.content)
    6.99 +  }
   6.100 +
   6.101 +  def handle_results(session: Session, id: Document_ID.Command, results: Command.Results): Context =
   6.102 +    (manager !? Handle_Results(session, id, results)).asInstanceOf[Context]
   6.103 +
   6.104 +  def generate_trace(results: Command.Results): Trace =
   6.105 +    (manager !? Generate_Trace(results)).asInstanceOf[Trace]
   6.106 +
   6.107 +  def clear_memory() =
   6.108 +    manager ! Clear_Memory
   6.109 +
   6.110 +  def send_reply(session: Session, serial: Long, answer: Answer) =
   6.111 +    manager ! Reply(session, serial, answer)
   6.112 +
   6.113 +  private val manager = actor {
   6.114 +    var contexts = Map.empty[Document_ID.Command, Context]
   6.115 +
   6.116 +    var memory_children = Map.empty[Long, Set[Long]]
   6.117 +    var memory = Map.empty[Index, Answer]
   6.118 +
   6.119 +    def find_question(serial: Long): Option[(Document_ID.Command, Question)] =
   6.120 +      contexts collectFirst {
   6.121 +        case (id, context) if context.questions contains serial =>
   6.122 +          (id, context.questions(serial))
   6.123 +      }
   6.124 +
   6.125 +    def do_cancel(serial: Long, id: Document_ID.Command)
   6.126 +    {
   6.127 +      // To save memory, we could try to remove empty contexts at this point.
   6.128 +      // However, if a new serial gets attached to the same command_id after we deleted
   6.129 +      // its context, its last_serial counter will start at 0 again, and we'll think the
   6.130 +      // old serials are actually new
   6.131 +      contexts += (id -> (contexts(id) - serial))
   6.132 +    }
   6.133 +
   6.134 +    def do_reply(session: Session, serial: Long, answer: Answer)
   6.135 +    {
   6.136 +      session.protocol_command("Document.simp_trace_reply", Properties.Value.Long(serial), answer.name)
   6.137 +    }
   6.138 +
   6.139 +    loop {
   6.140 +      react {
   6.141 +        case Handle_Results(session, id, results) =>
   6.142 +          var new_context = contexts.getOrElse(id, Context())
   6.143 +          var new_serial = new_context.last_serial
   6.144 +
   6.145 +          for ((serial, result) <- results.entries if serial > new_context.last_serial)
   6.146 +          {
   6.147 +            result match {
   6.148 +              case Simp_Trace_Item(markup, data) =>
   6.149 +                import Simp_Trace_Item._
   6.150 +
   6.151 +                memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
   6.152 +
   6.153 +                markup match {
   6.154 +
   6.155 +                  case STEP =>
   6.156 +                    val index = Index.of_data(data)
   6.157 +                    memory.get(index) match {
   6.158 +                      case None =>
   6.159 +                        new_context += Question(data, Answer.step.all, Answer.step.default)
   6.160 +                      case Some(answer) =>
   6.161 +                        do_reply(session, serial, answer)
   6.162 +                    }
   6.163 +
   6.164 +                  case HINT =>
   6.165 +                    data.props match {
   6.166 +                      case Markup.Success(false) =>
   6.167 +                        results.get(data.parent) match {
   6.168 +                          case Some(Simp_Trace_Item(STEP, _)) =>
   6.169 +                            new_context += Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
   6.170 +                          case _ =>
   6.171 +                            // unknown, better send a default reply
   6.172 +                            do_reply(session, data.serial, Answer.hint_fail.default)
   6.173 +                        }
   6.174 +                      case _ =>
   6.175 +                    }
   6.176 +
   6.177 +                  case IGNORE =>
   6.178 +                    // At this point, we know that the parent of this 'IGNORE' entry is a 'STEP'
   6.179 +                    // entry, and that that 'STEP' entry is about to be replayed. Hence, we need
   6.180 +                    // to selectively purge the replies which have been memorized, going down from
   6.181 +                    // the parent to all leaves.
   6.182 +
   6.183 +                    @tailrec
   6.184 +                    def purge(queue: Vector[Long]): Unit =
   6.185 +                      queue match {
   6.186 +                        case s +: rest =>
   6.187 +                          for (Simp_Trace_Item(STEP, data) <- results.get(s))
   6.188 +                            memory -= Index.of_data(data)
   6.189 +                          val children = memory_children.getOrElse(s, Set.empty)
   6.190 +                          memory_children -= s
   6.191 +                          purge(rest ++ children.toVector)
   6.192 +                        case _ =>
   6.193 +                      }
   6.194 +
   6.195 +                    purge(Vector(data.parent))
   6.196 +
   6.197 +                  case _ =>
   6.198 +                }
   6.199 +
   6.200 +              case _ =>
   6.201 +            }
   6.202 +
   6.203 +            new_serial = serial
   6.204 +          }
   6.205 +
   6.206 +          new_context = new_context.with_serial(new_serial)
   6.207 +          contexts += (id -> new_context)
   6.208 +          reply(new_context)
   6.209 +
   6.210 +        case Generate_Trace(results) =>
   6.211 +          // Since there are potentially lots of trace messages, we do not cache them here again.
   6.212 +          // Instead, everytime the trace is being requested, we re-assemble it based on the
   6.213 +          // current results.
   6.214 +
   6.215 +          val items =
   6.216 +            for { (_, Simp_Trace_Item(_, data)) <- results.entries }
   6.217 +              yield data
   6.218 +
   6.219 +          reply(Trace(items.toList))
   6.220 +
   6.221 +        case Cancel(serial) =>
   6.222 +          find_question(serial) match {
   6.223 +            case Some((id, _)) =>
   6.224 +              do_cancel(serial, id)
   6.225 +            case None =>
   6.226 +              System.err.println("handle_cancel: unknown serial " + serial)
   6.227 +          }
   6.228 +
   6.229 +        case Clear_Memory =>
   6.230 +          memory_children = Map.empty
   6.231 +          memory = Map.empty
   6.232 +
   6.233 +        case Stop =>
   6.234 +          contexts = Map.empty
   6.235 +          exit("Simplifier_Trace: manager actor stopped")
   6.236 +
   6.237 +        case Reply(session, serial, answer) =>
   6.238 +          find_question(serial) match {
   6.239 +            case Some((id, Question(data, _, _))) =>
   6.240 +              if (data.markup == Markup.Simp_Trace_Item.STEP)
   6.241 +              {
   6.242 +                val index = Index.of_data(data)
   6.243 +                memory += (index -> answer)
   6.244 +              }
   6.245 +              do_cancel(serial, id)
   6.246 +            case None =>
   6.247 +              System.err.println("send_reply: unknown serial " + serial)
   6.248 +          }
   6.249 +
   6.250 +          do_reply(session, serial, answer)
   6.251 +          session.trace_events.event(Event)
   6.252 +
   6.253 +        case bad =>
   6.254 +          System.err.println("context_manager: bad message " + bad)
   6.255 +      }
   6.256 +    }
   6.257 +  }
   6.258 +
   6.259 +
   6.260 +  /* protocol handler */
   6.261  
   6.262    class Handler extends Session.Protocol_Handler
   6.263    {
   6.264 -    val functions = Map.empty[String, (Session.Prover, Isabelle_Process.Protocol_Output) => Boolean]
   6.265 +    private def cancel(
   6.266 +      prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean =
   6.267 +      msg.properties match {
   6.268 +        case Markup.Cancel_Simp_Trace(serial) =>
   6.269 +          manager ! Cancel(serial)
   6.270 +          true
   6.271 +        case _ =>
   6.272 +          false
   6.273 +      }
   6.274 +
   6.275 +    override def stop(prover: Session.Prover) =
   6.276 +    {
   6.277 +      manager ! Clear_Memory
   6.278 +      manager ! Stop
   6.279 +    }
   6.280 +
   6.281 +    val functions = Map(
   6.282 +      Markup.CANCEL_SIMP_TRACE -> cancel _)
   6.283    }
   6.284 +
   6.285  }
     7.1 --- a/src/Pure/raw_simplifier.ML	Tue Feb 04 01:35:48 2014 +0100
     7.2 +++ b/src/Pure/raw_simplifier.ML	Tue Feb 04 09:04:59 2014 +0000
     7.3 @@ -17,6 +17,7 @@
     7.4    val simp_trace: bool Config.T
     7.5    type cong_name = bool * string
     7.6    type rrule
     7.7 +  val mk_rrules: Proof.context -> thm list -> rrule list
     7.8    val eq_rrule: rrule * rrule -> bool
     7.9    type proc
    7.10    type solver
    7.11 @@ -571,6 +572,12 @@
    7.12  fun extract_safe_rrules ctxt thm =
    7.13    maps (orient_rrule ctxt) (extract_rews ctxt [thm]);
    7.14  
    7.15 +fun mk_rrules ctxt thms =
    7.16 +  let
    7.17 +    val rews = extract_rews ctxt thms
    7.18 +    val raw_rrules = flat (map (mk_rrule ctxt) rews)
    7.19 +  in map mk_rrule2 raw_rrules end
    7.20 +
    7.21  
    7.22  (* add/del rules explicitly *)
    7.23  
    7.24 @@ -588,7 +595,6 @@
    7.25  fun add_simp thm ctxt = ctxt addsimps [thm];
    7.26  fun del_simp thm ctxt = ctxt delsimps [thm];
    7.27  
    7.28 -
    7.29  (* congs *)
    7.30  
    7.31  local
    7.32 @@ -814,7 +820,7 @@
    7.33  
    7.34  type trace_ops =
    7.35   {trace_invoke: {depth: int, term: term} -> Proof.context -> Proof.context,
    7.36 -  trace_apply: {unconditional: bool, term: term, thm: thm, name: string} ->
    7.37 +  trace_apply: {unconditional: bool, term: term, thm: thm, rrule: rrule} ->
    7.38      Proof.context -> (Proof.context -> (thm * term) option) -> (thm * term) option};
    7.39  
    7.40  structure Trace_Ops = Theory_Data
    7.41 @@ -919,8 +925,9 @@
    7.42      val eta_thm = Thm.eta_conversion t;
    7.43      val eta_t' = Thm.rhs_of eta_thm;
    7.44      val eta_t = term_of eta_t';
    7.45 -    fun rew {thm, name, lhs, elhs, extra, fo, perm} =
    7.46 +    fun rew rrule =
    7.47        let
    7.48 +        val {thm, name, lhs, elhs, extra, fo, perm} = rrule
    7.49          val prop = Thm.prop_of thm;
    7.50          val (rthm, elhs') =
    7.51            if maxt = ~1 orelse not extra then (thm, elhs)
    7.52 @@ -932,7 +939,7 @@
    7.53          val prop' = Thm.prop_of thm';
    7.54          val unconditional = (Logic.count_prems prop' = 0);
    7.55          val (lhs', rhs') = Logic.dest_equals (Logic.strip_imp_concl prop');
    7.56 -        val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', name = name};
    7.57 +        val trace_args = {unconditional = unconditional, term = eta_t, thm = thm', rrule = rrule};
    7.58        in
    7.59          if perm andalso not (termless (rhs', lhs'))
    7.60          then
     8.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Tue Feb 04 01:35:48 2014 +0100
     8.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Tue Feb 04 09:04:59 2014 +0000
     8.3 @@ -39,6 +39,8 @@
     8.4    "src/rich_text_area.scala"
     8.5    "src/scala_console.scala"
     8.6    "src/sledgehammer_dockable.scala"
     8.7 +  "src/simplifier_trace_dockable.scala"
     8.8 +  "src/simplifier_trace_window.scala"
     8.9    "src/symbols_dockable.scala"
    8.10    "src/syslog_dockable.scala"
    8.11    "src/text_overview.scala"
     9.1 --- a/src/Tools/jEdit/src/Isabelle.props	Tue Feb 04 01:35:48 2014 +0100
     9.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Tue Feb 04 09:04:59 2014 +0000
     9.3 @@ -37,6 +37,7 @@
     9.4    isabelle.protocol-panel \
     9.5    isabelle.raw-output-panel \
     9.6    isabelle.sledgehammer-panel \
     9.7 +  isabelle.simp-trace-panel \
     9.8    isabelle.symbols-panel \
     9.9    isabelle.syslog-panel \
    9.10    isabelle.theories-panel \
    9.11 @@ -47,6 +48,7 @@
    9.12  isabelle.output-panel.label=Output panel
    9.13  isabelle.protocol-panel.label=Protocol panel
    9.14  isabelle.raw-output-panel.label=Raw Output panel
    9.15 +isabelle.simp-trace-panel.label=Simplifier trace panel
    9.16  isabelle.sledgehammer-panel.label=Sledgehammer panel
    9.17  isabelle.symbols-panel.label=Symbols panel
    9.18  isabelle.syslog-panel.label=Syslog panel
    9.19 @@ -59,6 +61,7 @@
    9.20  isabelle-info.title=Info
    9.21  isabelle-monitor.title=Monitor
    9.22  isabelle-output.title=Output
    9.23 +isabelle-simp-trace.title=Simplifier trace
    9.24  isabelle-protocol.title=Protocol
    9.25  isabelle-raw-output.title=Raw Output
    9.26  isabelle-documentation.title=Documentation
    10.1 --- a/src/Tools/jEdit/src/actions.xml	Tue Feb 04 01:35:48 2014 +0100
    10.2 +++ b/src/Tools/jEdit/src/actions.xml	Tue Feb 04 09:04:59 2014 +0000
    10.3 @@ -42,6 +42,11 @@
    10.4  			wm.addDockableWindow("isabelle-raw-output");
    10.5  		</CODE>
    10.6  	</ACTION>
    10.7 +	<ACTION NAME="isabelle.simp-trace-panel">
    10.8 +		<CODE>
    10.9 +			wm.addDockableWindow("isabelle-simp-trace");
   10.10 +		</CODE>
   10.11 +	</ACTION>
   10.12  	<ACTION NAME="isabelle.protocol-panel">
   10.13  		<CODE>
   10.14  			wm.addDockableWindow("isabelle-protocol");
   10.15 @@ -147,4 +152,4 @@
   10.16  	    isabelle.jedit.Isabelle.input_bsup(textArea);
   10.17  	  </CODE>
   10.18  	</ACTION>
   10.19 -</ACTIONS>
   10.20 \ No newline at end of file
   10.21 +</ACTIONS>
    11.1 --- a/src/Tools/jEdit/src/active.scala	Tue Feb 04 01:35:48 2014 +0100
    11.2 +++ b/src/Tools/jEdit/src/active.scala	Tue Feb 04 09:04:59 2014 +0000
    11.3 @@ -61,6 +61,9 @@
    11.4                      else text_area.setSelectedText(text)
    11.5                  }
    11.6  
    11.7 +              case Markup.Simp_Trace(serial, answer) =>
    11.8 +                Simplifier_Trace.send_reply(PIDE.session, serial, answer)
    11.9 +
   11.10                case Protocol.Dialog(id, serial, result) =>
   11.11                  model.session.dialog_result(id, serial, result)
   11.12  
   11.13 @@ -72,4 +75,3 @@
   11.14      }
   11.15    }
   11.16  }
   11.17 -
    12.1 --- a/src/Tools/jEdit/src/dockables.xml	Tue Feb 04 01:35:48 2014 +0100
    12.2 +++ b/src/Tools/jEdit/src/dockables.xml	Tue Feb 04 09:04:59 2014 +0000
    12.3 @@ -41,4 +41,7 @@
    12.4  	<DOCKABLE NAME="isabelle-symbols" MOVABLE="TRUE">
    12.5  		new isabelle.jedit.Symbols_Dockable(view, position);
    12.6  	</DOCKABLE>
    12.7 -</DOCKABLES>
    12.8 \ No newline at end of file
    12.9 +	<DOCKABLE NAME="isabelle-simp-trace" MOVABLE="TRUE">
   12.10 +		new isabelle.jedit.Simplifier_Trace_Dockable(view, position);
   12.11 +	</DOCKABLE>
   12.12 +</DOCKABLES>
    13.1 --- a/src/Tools/jEdit/src/isabelle.scala	Tue Feb 04 01:35:48 2014 +0100
    13.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Feb 04 09:04:59 2014 +0000
    13.3 @@ -81,6 +81,12 @@
    13.4        case _ => None
    13.5      }
    13.6  
    13.7 +  def docked_simplifier_trace(view: View): Option[Simplifier_Trace_Dockable] =
    13.8 +    wm(view).getDockableWindow("isabelle-simp-trace") match {
    13.9 +      case dockable: Simplifier_Trace_Dockable => Some(dockable)
   13.10 +      case _ => None
   13.11 +    }
   13.12 +
   13.13    def docked_protocol(view: View): Option[Protocol_Dockable] =
   13.14      wm(view).getDockableWindow("isabelle-protocol") match {
   13.15        case dockable: Protocol_Dockable => Some(dockable)
    14.1 --- a/src/Tools/jEdit/src/jEdit.props	Tue Feb 04 01:35:48 2014 +0100
    14.2 +++ b/src/Tools/jEdit/src/jEdit.props	Tue Feb 04 09:04:59 2014 +0000
    14.3 @@ -189,6 +189,7 @@
    14.4  isabelle-output.height=174
    14.5  isabelle-output.width=412
    14.6  isabelle-sledgehammer.dock-position=bottom
    14.7 +isabelle-simp-trace.dock-position=bottom
    14.8  isabelle-symbols.dock-position=bottom
    14.9  isabelle-theories.dock-position=right
   14.10  isabelle.complete.label=Complete Isabelle text
    15.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Feb 04 01:35:48 2014 +0100
    15.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Feb 04 09:04:59 2014 +0000
    15.3 @@ -270,7 +270,7 @@
    15.4  
    15.5  
    15.6    private val active_include =
    15.7 -    Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG)
    15.8 +    Set(Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.DIALOG, Markup.SIMP_TRACE)
    15.9  
   15.10    def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
   15.11      snapshot.select_markup(range, Some(active_include), command_state =>
   15.12 @@ -281,7 +281,8 @@
   15.13            case Text.Info(info_range, elem) =>
   15.14              if (elem.name == Markup.BROWSER ||
   15.15                  elem.name == Markup.GRAPHVIEW ||
   15.16 -                elem.name == Markup.SENDBACK)
   15.17 +                elem.name == Markup.SENDBACK ||
   15.18 +                elem.name == Markup.SIMP_TRACE)
   15.19                Some(Text.Info(snapshot.convert(info_range), elem))
   15.20              else None
   15.21          }) match { case Text.Info(_, info) :: _ => Some(info) case _ => None }
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Tue Feb 04 09:04:59 2014 +0000
    16.3 @@ -0,0 +1,222 @@
    16.4 +/*  Title:      Tools/jEdit/src/simplifier_trace_dockable.scala
    16.5 +    Author:     Lars Hupel
    16.6 +
    16.7 +Dockable window with interactive simplifier trace.
    16.8 +*/
    16.9 +
   16.10 +package isabelle.jedit
   16.11 +
   16.12 +
   16.13 +import isabelle._
   16.14 +
   16.15 +import scala.actors.Actor._
   16.16 +
   16.17 +import scala.swing.{Button, CheckBox, Orientation, Separator}
   16.18 +import scala.swing.event.ButtonClicked
   16.19 +
   16.20 +import java.awt.BorderLayout
   16.21 +import java.awt.event.{ComponentEvent, ComponentAdapter}
   16.22 +
   16.23 +import org.gjt.sp.jedit.View
   16.24 +
   16.25 +class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position)
   16.26 +{
   16.27 +  Swing_Thread.require()
   16.28 +
   16.29 +  /* component state -- owned by Swing thread */
   16.30 +
   16.31 +  private var current_snapshot = Document.State.init.snapshot()
   16.32 +  private var current_state = Command.empty.init_state
   16.33 +  private var current_id = 0L
   16.34 +  private var do_update = true
   16.35 +  private var do_auto_reply = false
   16.36 +
   16.37 +
   16.38 +  private val text_area = new Pretty_Text_Area(view)
   16.39 +  set_content(text_area)
   16.40 +
   16.41 +  private def get_content(snapshot: Document.Snapshot, question: Simplifier_Trace.Question): XML.Tree =
   16.42 +  {
   16.43 +    val data = question.data
   16.44 +
   16.45 +    def make_button(answer: Simplifier_Trace.Answer): XML.Tree =
   16.46 +      XML.Wrapped_Elem(
   16.47 +        Markup(Markup.SIMP_TRACE, Markup.Serial(data.serial) ::: Markup.Name(answer.name)),
   16.48 +        Nil,
   16.49 +        List(XML.Text(answer.string))
   16.50 +      )
   16.51 +
   16.52 +    def make_block(body: XML.Body): XML.Body =
   16.53 +      List(Pretty.Block(0, body))
   16.54 +
   16.55 +    val all = Pretty.separate(
   16.56 +      XML.Text(data.text) ::
   16.57 +      data.content :::
   16.58 +      make_block(Library.separate(XML.Text(", "), question.answers map make_button))
   16.59 +    )
   16.60 +
   16.61 +    XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(all)))
   16.62 +  }
   16.63 +
   16.64 +  private def set_context(snapshot: Document.Snapshot, context: Simplifier_Trace.Context)
   16.65 +  {
   16.66 +    Swing_Thread.require()
   16.67 +    val questions = context.questions.values
   16.68 +    if (do_auto_reply && !questions.isEmpty)
   16.69 +    {
   16.70 +      questions.foreach(q => Simplifier_Trace.send_reply(PIDE.session, q.data.serial, q.default_answer))
   16.71 +      handle_update(do_update)
   16.72 +    }
   16.73 +    else
   16.74 +    {
   16.75 +      val contents = Pretty.separate(questions.map(get_content(snapshot, _))(collection.breakOut))
   16.76 +      text_area.update(snapshot, Command.Results.empty, contents)
   16.77 +      do_paint()
   16.78 +    }
   16.79 +  }
   16.80 +
   16.81 +  private def show_trace()
   16.82 +  {
   16.83 +    val trace = Simplifier_Trace.generate_trace(current_state.results)
   16.84 +    new Simplifier_Trace_Window(view, current_snapshot, trace)
   16.85 +  }
   16.86 +
   16.87 +  private def do_paint()
   16.88 +  {
   16.89 +    Swing_Thread.later {
   16.90 +        text_area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
   16.91 +    }
   16.92 +  }
   16.93 +
   16.94 +  private def update_contents()
   16.95 +  {
   16.96 +    set_context(
   16.97 +      current_snapshot,
   16.98 +      Simplifier_Trace.handle_results(PIDE.session, current_id, current_state.results)
   16.99 +    )
  16.100 +  }
  16.101 +
  16.102 +  private def handle_resize()
  16.103 +  {
  16.104 +    do_paint()
  16.105 +  }
  16.106 +
  16.107 +  private def handle_update(follow: Boolean)
  16.108 +  {
  16.109 +    val (new_snapshot, new_state, new_id) =
  16.110 +      PIDE.editor.current_node_snapshot(view) match {
  16.111 +        case Some(snapshot) =>
  16.112 +          if (follow && !snapshot.is_outdated) {
  16.113 +            PIDE.editor.current_command(view, snapshot) match {
  16.114 +              case Some(cmd) =>
  16.115 +                (snapshot, snapshot.state.command_state(snapshot.version, cmd), cmd.id)
  16.116 +              case None =>
  16.117 +                (Document.State.init.snapshot(), Command.empty.init_state, 0L)
  16.118 +            }
  16.119 +          }
  16.120 +          else (current_snapshot, current_state, current_id)
  16.121 +        case None => (current_snapshot, current_state, current_id)
  16.122 +      }
  16.123 +
  16.124 +    current_snapshot = new_snapshot
  16.125 +    current_state = new_state
  16.126 +    current_id = new_id
  16.127 +    update_contents()
  16.128 +  }
  16.129 +
  16.130 +
  16.131 +  /* main actor */
  16.132 +
  16.133 +  private val main_actor = actor {
  16.134 +    loop {
  16.135 +      react {
  16.136 +        case _: Session.Global_Options =>
  16.137 +          Swing_Thread.later { handle_resize() }
  16.138 +        case changed: Session.Commands_Changed =>
  16.139 +          Swing_Thread.later { handle_update(do_update) }
  16.140 +        case Session.Caret_Focus =>
  16.141 +          Swing_Thread.later { handle_update(do_update) }
  16.142 +        case Simplifier_Trace.Event =>
  16.143 +          Swing_Thread.later { handle_update(do_update) }
  16.144 +        case bad => System.err.println("Simplifier_Trace_Dockable: ignoring bad message " + bad)
  16.145 +      }
  16.146 +    }
  16.147 +  }
  16.148 +
  16.149 +  override def init()
  16.150 +  {
  16.151 +    Swing_Thread.require()
  16.152 +
  16.153 +    PIDE.session.global_options += main_actor
  16.154 +    PIDE.session.commands_changed += main_actor
  16.155 +    PIDE.session.caret_focus += main_actor
  16.156 +    PIDE.session.trace_events += main_actor
  16.157 +    handle_update(true)
  16.158 +  }
  16.159 +
  16.160 +  override def exit()
  16.161 +  {
  16.162 +    Swing_Thread.require()
  16.163 +
  16.164 +    PIDE.session.global_options -= main_actor
  16.165 +    PIDE.session.commands_changed -= main_actor
  16.166 +    PIDE.session.caret_focus -= main_actor
  16.167 +    PIDE.session.trace_events -= main_actor
  16.168 +    delay_resize.revoke()
  16.169 +  }
  16.170 +
  16.171 +
  16.172 +  /* resize */
  16.173 +
  16.174 +  private val delay_resize =
  16.175 +    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
  16.176 +
  16.177 +  addComponentListener(new ComponentAdapter {
  16.178 +    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
  16.179 +    override def componentShown(e: ComponentEvent)   { delay_resize.invoke() }
  16.180 +  })
  16.181 +
  16.182 +
  16.183 +  /* controls */
  16.184 +
  16.185 +  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
  16.186 +    new CheckBox("Auto update") {
  16.187 +      selected = do_update
  16.188 +      reactions += {
  16.189 +        case ButtonClicked(_) =>
  16.190 +          do_update = this.selected
  16.191 +          handle_update(do_update)
  16.192 +      }
  16.193 +    },
  16.194 +    new Button("Update") {
  16.195 +      reactions += {
  16.196 +        case ButtonClicked(_) =>
  16.197 +          handle_update(true)
  16.198 +      }
  16.199 +    },
  16.200 +    new Separator(Orientation.Vertical),
  16.201 +    new CheckBox("Auto reply") {
  16.202 +      selected = do_auto_reply
  16.203 +      reactions += {
  16.204 +        case ButtonClicked(_) =>
  16.205 +          do_auto_reply = this.selected
  16.206 +          handle_update(do_update)
  16.207 +      }
  16.208 +    },
  16.209 +    new Separator(Orientation.Vertical),
  16.210 +    new Button("Show trace") {
  16.211 +      reactions += {
  16.212 +        case ButtonClicked(_) =>
  16.213 +          show_trace()
  16.214 +      }
  16.215 +    },
  16.216 +    new Button("Clear memory") {
  16.217 +      reactions += {
  16.218 +        case ButtonClicked(_) =>
  16.219 +          Simplifier_Trace.clear_memory()
  16.220 +      }
  16.221 +    }
  16.222 +  )
  16.223 +
  16.224 +  add(controls.peer, BorderLayout.NORTH)
  16.225 +}
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala	Tue Feb 04 09:04:59 2014 +0000
    17.3 @@ -0,0 +1,237 @@
    17.4 +/*  Title:      Tools/jEdit/src/simplifier_trace_window.scala
    17.5 +    Author:     Lars Hupel
    17.6 +
    17.7 +Trace window with tree-style view of the simplifier trace.
    17.8 +*/
    17.9 +
   17.10 +package isabelle.jedit
   17.11 +
   17.12 +
   17.13 +import isabelle._
   17.14 +
   17.15 +import scala.annotation.tailrec
   17.16 +
   17.17 +import scala.collection.immutable.SortedMap
   17.18 +
   17.19 +import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField}
   17.20 +import scala.swing.event.{Key, KeyPressed}
   17.21 +
   17.22 +import scala.util.matching.Regex
   17.23 +
   17.24 +import java.awt.BorderLayout
   17.25 +import java.awt.event.{ComponentEvent, ComponentAdapter}
   17.26 +
   17.27 +import javax.swing.SwingUtilities
   17.28 +
   17.29 +import org.gjt.sp.jedit.View
   17.30 +
   17.31 +private object Simplifier_Trace_Window
   17.32 +{
   17.33 +
   17.34 +  import Markup.Simp_Trace_Item
   17.35 +
   17.36 +  sealed trait Trace_Tree
   17.37 +  {
   17.38 +    var children: SortedMap[Long, Elem_Tree] = SortedMap.empty
   17.39 +    val serial: Long
   17.40 +    val parent: Option[Trace_Tree]
   17.41 +    var hints: List[Simp_Trace_Item.Data]
   17.42 +    def set_interesting(): Unit
   17.43 +  }
   17.44 +
   17.45 +  final class Root_Tree(val serial: Long) extends Trace_Tree
   17.46 +  {
   17.47 +    val parent = None
   17.48 +    val hints = Nil
   17.49 +    def hints_=(xs: List[Simp_Trace_Item.Data]) = throw new IllegalStateException("Root_Tree.hints")
   17.50 +    def set_interesting() = ()
   17.51 +
   17.52 +    def format(regex: Option[Regex]): XML.Body =
   17.53 +      Pretty.separate(children.values.map(_.format(regex)._2)(collection.breakOut))
   17.54 +  }
   17.55 +
   17.56 +  final class Elem_Tree(data: Simp_Trace_Item.Data, val parent: Option[Trace_Tree]) extends Trace_Tree
   17.57 +  {
   17.58 +    val serial = data.serial
   17.59 +    var hints = List.empty[Simp_Trace_Item.Data]
   17.60 +    var interesting: Boolean = false
   17.61 +
   17.62 +    def set_interesting(): Unit =
   17.63 +      if (!interesting)
   17.64 +      {
   17.65 +        interesting = true
   17.66 +        parent match {
   17.67 +          case Some(p) =>
   17.68 +            p.set_interesting()
   17.69 +          case None =>
   17.70 +        }
   17.71 +      }
   17.72 +
   17.73 +    def format(regex: Option[Regex]): (Boolean, XML.Tree) =
   17.74 +    {
   17.75 +      def format_child(child: Elem_Tree): Option[XML.Tree] = child.format(regex) match {
   17.76 +        case (false, _) =>
   17.77 +          None
   17.78 +        case (true, res) =>
   17.79 +          Some(XML.Elem(Markup(Markup.ITEM, Nil), List(res)))
   17.80 +      }
   17.81 +
   17.82 +      def format_hint(data: Simp_Trace_Item.Data): XML.Tree =
   17.83 +        Pretty.block(Pretty.separate(
   17.84 +          XML.Text(data.text) ::
   17.85 +          data.content
   17.86 +        ))
   17.87 +
   17.88 +      def body_contains(regex: Regex, body: XML.Body): Boolean =
   17.89 +        body.exists(tree => regex.findFirstIn(XML.content(tree)).isDefined)
   17.90 +
   17.91 +      val children_bodies: XML.Body =
   17.92 +        children.values.filter(_.interesting).flatMap(format_child).toList
   17.93 +
   17.94 +      lazy val hint_bodies: XML.Body =
   17.95 +        hints.reverse.map(format_hint)
   17.96 +
   17.97 +      val eligible = regex match {
   17.98 +        case None =>
   17.99 +          true
  17.100 +        case Some(r) =>
  17.101 +          body_contains(r, data.content) || hints.exists(h => body_contains(r, h.content))
  17.102 +      }
  17.103 +
  17.104 +      val all =
  17.105 +        if (eligible)
  17.106 +          XML.Text(data.text) :: data.content ::: children_bodies ::: hint_bodies
  17.107 +        else
  17.108 +          XML.Text(data.text) :: children_bodies
  17.109 +
  17.110 +      val res = XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(Pretty.separate(all))))
  17.111 +
  17.112 +      (eligible || children_bodies != Nil, res)
  17.113 +    }
  17.114 +  }
  17.115 +
  17.116 +  @tailrec
  17.117 +  def walk_trace(rest: List[Simp_Trace_Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
  17.118 +    rest match {
  17.119 +      case Nil =>
  17.120 +        ()
  17.121 +      case head :: tail =>
  17.122 +        lookup.get(head.parent) match {
  17.123 +          case Some(parent) =>
  17.124 +            if (head.markup == Simp_Trace_Item.HINT)
  17.125 +            {
  17.126 +              parent.hints ::= head
  17.127 +              walk_trace(tail, lookup)
  17.128 +            }
  17.129 +            else if (head.markup == Simp_Trace_Item.IGNORE)
  17.130 +            {
  17.131 +              parent.parent match {
  17.132 +                case None =>
  17.133 +                  System.err.println("Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
  17.134 +                case Some(tree) =>
  17.135 +                  tree.children -= head.parent
  17.136 +                  walk_trace(tail, lookup) // FIXME discard from lookup
  17.137 +              }
  17.138 +            }
  17.139 +            else
  17.140 +            {
  17.141 +              val entry = new Elem_Tree(head, Some(parent))
  17.142 +              parent.children += ((head.serial, entry))
  17.143 +              if (head.markup == Simp_Trace_Item.STEP || head.markup == Simp_Trace_Item.LOG)
  17.144 +                entry.set_interesting()
  17.145 +              walk_trace(tail, lookup + (head.serial -> entry))
  17.146 +            }
  17.147 +
  17.148 +          case None =>
  17.149 +            System.err.println("Simplifier_Trace_Window: unknown parent " + head.parent)
  17.150 +        }
  17.151 +    }
  17.152 +
  17.153 +}
  17.154 +
  17.155 +class Simplifier_Trace_Window(view: View, snapshot: Document.Snapshot, trace: Simplifier_Trace.Trace) extends Frame
  17.156 +{
  17.157 +
  17.158 +  import Simplifier_Trace_Window._
  17.159 +
  17.160 +  Swing_Thread.require()
  17.161 +
  17.162 +  val area = new Pretty_Text_Area(view)
  17.163 +
  17.164 +  size = new Dimension(500, 500)
  17.165 +  contents = new BorderPanel {
  17.166 +    layout(Component.wrap(area)) = BorderPanel.Position.Center
  17.167 +  }
  17.168 +
  17.169 +  private val tree = trace.entries.headOption match {
  17.170 +    case Some(first) =>
  17.171 +      val tree = new Root_Tree(first.parent)
  17.172 +      walk_trace(trace.entries, Map(first.parent -> tree))
  17.173 +      tree
  17.174 +    case None =>
  17.175 +      new Root_Tree(0)
  17.176 +  }
  17.177 +
  17.178 +  do_update(None)
  17.179 +  open()
  17.180 +  do_paint()
  17.181 +
  17.182 +  def do_update(regex: Option[Regex])
  17.183 +  {
  17.184 +    val xml = tree.format(regex)
  17.185 +    area.update(snapshot, Command.Results.empty, xml)
  17.186 +  }
  17.187 +
  17.188 +  def do_paint()
  17.189 +  {
  17.190 +    Swing_Thread.later {
  17.191 +      area.resize(Rendering.font_family(), Rendering.font_size("jedit_font_scale").round)
  17.192 +    }
  17.193 +  }
  17.194 +
  17.195 +  def handle_resize()
  17.196 +  {
  17.197 +    do_paint()
  17.198 +  }
  17.199 +
  17.200 +
  17.201 +  /* resize */
  17.202 +
  17.203 +  private val delay_resize =
  17.204 +    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
  17.205 +
  17.206 +  peer.addComponentListener(new ComponentAdapter {
  17.207 +    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
  17.208 +    override def componentShown(e: ComponentEvent)   { delay_resize.invoke() }
  17.209 +  })
  17.210 +
  17.211 +
  17.212 +  /* controls */
  17.213 +
  17.214 +  val use_regex = new CheckBox("Regex")
  17.215 +
  17.216 +  private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(
  17.217 +    new Label {
  17.218 +      text = "Search"
  17.219 +    },
  17.220 +    new TextField(30) {
  17.221 +      listenTo(keys)
  17.222 +      reactions += {
  17.223 +        case KeyPressed(_, Key.Enter, 0, _) =>
  17.224 +          val input = text.trim
  17.225 +          val regex =
  17.226 +            if (input.isEmpty)
  17.227 +              None
  17.228 +            else if (use_regex.selected)
  17.229 +              Some(input.r)
  17.230 +            else
  17.231 +              Some(java.util.regex.Pattern.quote(input).r)
  17.232 +          do_update(regex)
  17.233 +          do_paint()
  17.234 +      }
  17.235 +    },
  17.236 +    use_regex
  17.237 +  )
  17.238 +
  17.239 +  peer.add(controls.peer, BorderLayout.NORTH)
  17.240 +}