# HG changeset patch
# User wenzelm
# Date 1405969067 -7200
# Node ID 5c3484b90d5c11f136e04009aede5bfadcf54365
# Parent  5efff4075b63db8455d55b3816b143d57c258f14# Parent  3a1b1bda702f8a0bf5b14228f52f72b18f2bd910
merged

diff -r 5efff4075b63 -r 5c3484b90d5c Admin/components/components.sha1
--- a/Admin/components/components.sha1	Mon Jul 21 18:04:08 2014 +0200
+++ b/Admin/components/components.sha1	Mon Jul 21 20:57:47 2014 +0200
@@ -26,6 +26,7 @@
 5080274f8721a18111a7f614793afe6c88726739  jdk-7u25.tar.gz
 dd24d63afd6d17b29ec9cb2b2464d4ff2e02de2c  jdk-7u40.tar.gz
 71b629b2ce83dbb69967c4785530afce1bec3809  jdk-7u60.tar.gz
+e119f4cbfa2a39a53b9578d165d0dc44b59527b7  jdk-7u65.tar.gz
 ec740ee9ffd43551ddf1e5b91641405116af6291  jdk-7u6.tar.gz
 7d5b152ac70f720bb9e783fa45ecadcf95069584  jdk-7u9.tar.gz
 5442f1015a0657259be0590b04572cd933431df7  jdk-8u11.tar.gz
diff -r 5efff4075b63 -r 5c3484b90d5c Admin/components/main
--- a/Admin/components/main	Mon Jul 21 18:04:08 2014 +0200
+++ b/Admin/components/main	Mon Jul 21 20:57:47 2014 +0200
@@ -3,7 +3,7 @@
 e-1.8
 exec_process-1.0.3
 Haskabelle-2013
-jdk-7u60
+jdk-7u65
 jedit_build-20140511
 jfreechart-1.0.14-1
 jortho-1.0-2
diff -r 5efff4075b63 -r 5c3484b90d5c Admin/java/build
--- a/Admin/java/build	Mon Jul 21 18:04:08 2014 +0200
+++ b/Admin/java/build	Mon Jul 21 20:57:47 2014 +0200
@@ -11,8 +11,8 @@
 
 ## parameters
 
-VERSION="8u11"
-FULL_VERSION="1.8.0_11"
+VERSION="7u65"
+FULL_VERSION="1.7.0_65"
 
 ARCHIVE_LINUX32="jdk-${VERSION}-linux-i586.tar.gz"
 ARCHIVE_LINUX64="jdk-${VERSION}-linux-x64.tar.gz"
@@ -113,7 +113,7 @@
     do
       if cmp -s "$FILE" "$OTHER"
       then
-        echo -n "."
+        echo -n "*"
         ln -f "$FILE" "$OTHER"
       fi
     done
diff -r 5efff4075b63 -r 5c3484b90d5c NEWS
--- a/NEWS	Mon Jul 21 18:04:08 2014 +0200
+++ b/NEWS	Mon Jul 21 20:57:47 2014 +0200
@@ -116,7 +116,7 @@
 "Detach" a copy where this makes sense.
 
 * New Simplifier Trace panel provides an interactive view of the
-simplification process, enabled by the "simplifier_trace" attribute
+simplification process, enabled by the "simp_trace_new" attribute
 within the context.
 
 
diff -r 5efff4075b63 -r 5c3484b90d5c src/Doc/Isar_Ref/Generic.thy
--- a/src/Doc/Isar_Ref/Generic.thy	Mon Jul 21 18:04:08 2014 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy	Mon Jul 21 20:57:47 2014 +0200
@@ -395,10 +395,12 @@
 subsection {* Simplification methods \label{sec:simp-meth} *}
 
 text {*
-  \begin{matharray}{rcl}
+  \begin{tabular}{rcll}
     @{method_def simp} & : & @{text method} \\
     @{method_def simp_all} & : & @{text method} \\
-  \end{matharray}
+    @{attribute_def simp_depth_limit} & : & @{text attribute} & default @{text 100} \\
+  \end{tabular}
+  \medskip
 
   @{rail \<open>
     (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * )
@@ -463,6 +465,9 @@
   The proof method fails if all subgoals remain unchanged after
   simplification.
 
+  \item @{attribute simp_depth_limit} limits the number of recursive
+  invocations of the Simplifier during conditional rewriting.
+
   \end{description}
 
   By default the Simplifier methods above take local assumptions fully
@@ -586,7 +591,7 @@
   apply simp
   oops
 
-text {* See also \secref{sec:simp-config} for options to enable
+text {* See also \secref{sec:simp-trace} for options to enable
   Simplifier trace mode, which often helps to diagnose problems with
   rewrite systems.
 *}
@@ -859,25 +864,32 @@
   reorientation and mutual simplification fail to apply.  *}
 
 
-subsection {* Configuration options \label{sec:simp-config} *}
+subsection {* Simplifier tracing and debugging \label{sec:simp-trace} *}
 
 text {*
   \begin{tabular}{rcll}
-    @{attribute_def simp_depth_limit} & : & @{text attribute} & default @{text 100} \\
     @{attribute_def simp_trace} & : & @{text attribute} & default @{text false} \\
     @{attribute_def simp_trace_depth_limit} & : & @{text attribute} & default @{text 1} \\
     @{attribute_def simp_debug} & : & @{text attribute} & default @{text false} \\
+    @{attribute_def simp_trace_new} & : & @{text attribute} \\
+    @{attribute_def simp_break} & : & @{text attribute} \\
   \end{tabular}
   \medskip
 
-  These configurations options control further aspects of the Simplifier.
-  See also \secref{sec:config}.
+  @{rail \<open>
+    @@{attribute simp_trace_new} ('interactive')? \<newline>
+      ('mode' '=' ('full' | 'normal'))? \<newline>
+      ('depth' '=' @{syntax nat})?
+    ;
+
+    @@{attribute simp_break} (@{syntax term}*)
+  \<close>}
+
+  These attributes and configurations options control various aspects of
+  Simplifier tracing and debugging.
 
   \begin{description}
 
-  \item @{attribute simp_depth_limit} limits the number of recursive
-  invocations of the Simplifier during conditional rewriting.
-
   \item @{attribute simp_trace} makes the Simplifier output internal
   operations.  This includes rewrite steps, but also bookkeeping like
   modifications of the simpset.
@@ -890,9 +902,30 @@
   information about internal operations.  This includes any attempted
   invocation of simplification procedures.
 
+  \item @{attribute simp_trace_new} controls Simplifier tracing within
+  Isabelle/PIDE applications, notably Isabelle/jEdit \cite{isabelle-jedit}.
+  This provides a hierarchical representation of the rewriting steps
+  performed by the Simplifier.
+
+  Users can configure the behaviour by specifying breakpoints, verbosity and
+  enabling or disabling the interactive mode. In normal verbosity (the
+  default), only rule applications matching a breakpoint will be shown to
+  the user. In full verbosity, all rule applications will be logged.
+  Interactive mode interrupts the normal flow of the Simplifier and defers
+  the decision how to continue to the user via some GUI dialog.
+
+  \item @{attribute simp_break} declares term or theorem breakpoints for
+  @{attribute simp_trace_new} as described above. Term breakpoints are
+  patterns which are checked for matches on the redex of a rule application.
+  Theorem breakpoints trigger when the corresponding theorem is applied in a
+  rewrite step. For example:
+
   \end{description}
 *}
 
+declare conjI [simp_break]
+declare [[simp_break "?x \<and> ?y"]]
+
 
 subsection {* Simplification procedures \label{sec:simproc} *}
 
diff -r 5efff4075b63 -r 5c3484b90d5c src/Doc/Isar_Ref/document/root.tex
--- a/src/Doc/Isar_Ref/document/root.tex	Mon Jul 21 18:04:08 2014 +0200
+++ b/src/Doc/Isar_Ref/document/root.tex	Mon Jul 21 20:57:47 2014 +0200
@@ -34,14 +34,15 @@
   Lucas Dixon,
   Florian Haftmann, \\
   Brian Huffman,
-  Gerwin Klein,
-  Alexander Krauss, \\
+  Lars Hupel,
+  Gerwin Klein, \\
+  Alexander Krauss,
   Ond\v{r}ej Kun\v{c}ar,
-  Andreas Lochbihler,
-  Tobias Nipkow, \\
+  Andreas Lochbihler, \\
+  Tobias Nipkow,
   Lars Noschinski,
-  David von Oheimb,
-  Larry Paulson, \\
+  David von Oheimb, \\
+  Larry Paulson,
   Sebastian Skalberg,
   Christian Sternagel
 }
diff -r 5efff4075b63 -r 5c3484b90d5c src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Mon Jul 21 18:04:08 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Mon Jul 21 20:57:47 2014 +0200
@@ -1225,6 +1225,12 @@
   situations, to tell that some language keywords should be excluded from
   further completion attempts. For example, @{verbatim ":"} within accepted
   Isar syntax looses its meaning as abbreviation for symbol @{text "\<in>"}.
+
+  \medskip The completion context is \emph{ignored} for built-in templates and
+  symbols in their explicit form ``@{verbatim "\<foobar>"}''; see also
+  \secref{sec:completion-varieties}. This allows to complete within broken
+  input that escapes its normal semantic context, e.g.\ antiquotations or
+  string literals in ML, which do not allow arbitrary backslash sequences.
 *}
 
 
diff -r 5efff4075b63 -r 5c3484b90d5c src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Mon Jul 21 18:04:08 2014 +0200
+++ b/src/Pure/General/completion.scala	Mon Jul 21 20:57:47 2014 +0200
@@ -11,6 +11,7 @@
 
 import scala.collection.immutable.SortedMap
 import scala.util.parsing.combinator.RegexParsers
+import scala.util.matching.Regex
 import scala.math.Ordering
 
 
@@ -219,6 +220,9 @@
   {
     override val whiteSpace = "".r
 
+    private val symbol_regex: Regex = """\\<\^?[A-Za-z0-9_']+>""".r
+    def is_symbol(s: CharSequence): Boolean = symbol_regex.pattern.matcher(s).matches
+
     private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
     private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
     private def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
@@ -231,16 +235,6 @@
     def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
     def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.'
 
-    def extend_word(text: CharSequence, offset: Text.Offset): Text.Offset =
-    {
-      val n = text.length
-      var i = offset
-      while (i < n && is_word_char(text.charAt(i))) i += 1
-      if (i < n && text.charAt(i) == '>' && read_symbol(text.subSequence(0, i + 1)).isDefined)
-        i + 1
-      else i
-    }
-
     def read_symbol(in: CharSequence): Option[String] =
     {
       val reverse_in = new Library.Reverse(in)
@@ -341,7 +335,6 @@
     start: Text.Offset,
     text: CharSequence,
     caret: Int,
-    extend_word: Boolean,
     language_context: Completion.Language_Context): Option[Completion.Result] =
   {
     def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
@@ -358,8 +351,11 @@
             case (a, _) :: _ =>
               val ok =
                 if (a == Completion.antiquote) language_context.antiquotes
-                else language_context.symbols || Completion.default_abbrs.exists(_._1 == a)
-              if (ok) Some(((a, abbrevs), caret))
+                else
+                  language_context.symbols ||
+                  Completion.default_abbrs.exists(_._1 == a) ||
+                  Completion.Word_Parsers.is_symbol(a)
+              if (ok) Some((a, abbrevs))
               else None
           }
         case _ => None
@@ -369,17 +365,10 @@
     val words_result =
       if (abbrevs_result.isDefined) None
       else {
-        val end =
-          if (extend_word) Completion.Word_Parsers.extend_word(text, caret)
-          else caret
         val result =
-          Completion.Word_Parsers.read_symbol(text.subSequence(0, end)) match {
+          Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match {
             case Some(symbol) => Some((symbol, ""))
-            case None =>
-              val word_context =
-                end < length && Completion.Word_Parsers.is_word_char(text.charAt(end))
-              if (word_context) None
-              else Completion.Word_Parsers.read_word(explicit, text.subSequence(0, end))
+            case None => Completion.Word_Parsers.read_word(explicit, text.subSequence(0, caret))
           }
         result.map(
           {
@@ -397,13 +386,13 @@
                     if ok
                     completion <- words_map.get_list(complete_word)
                   } yield (complete_word, completion)
-              (((full_word, completions), end))
+              ((full_word, completions))
           })
       }
 
     (abbrevs_result orElse words_result) match {
-      case Some(((original, completions), end)) if !completions.isEmpty =>
-        val range = Text.Range(- original.length, 0) + end + start
+      case Some((original, completions)) if !completions.isEmpty =>
+        val range = Text.Range(- original.length, 0) + caret + start
         val immediate =
           explicit ||
             (!Completion.Word_Parsers.is_word(original) &&
diff -r 5efff4075b63 -r 5c3484b90d5c src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Jul 21 18:04:08 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Mon Jul 21 20:57:47 2014 +0200
@@ -185,6 +185,7 @@
   val use_theories_result: string -> bool -> Properties.T
   val print_operationsN: string
   val print_operations: Properties.T
+  val simp_trace_panelN: string
   val simp_trace_logN: string
   val simp_trace_stepN: string
   val simp_trace_recurseN: string
@@ -586,6 +587,8 @@
 
 (* simplifier trace *)
 
+val simp_trace_panelN = "simp_trace_panel";
+
 val simp_trace_logN = "simp_trace_log";
 val simp_trace_stepN = "simp_trace_step";
 val simp_trace_recurseN = "simp_trace_recurse";
diff -r 5efff4075b63 -r 5c3484b90d5c src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Mon Jul 21 18:04:08 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Mon Jul 21 20:57:47 2014 +0200
@@ -464,7 +464,7 @@
 
   /* simplifier trace */
 
-  val SIMP_TRACE = "simp_trace"
+  val SIMP_TRACE_PANEL = "simp_trace_panel"
 
   val SIMP_TRACE_LOG = "simp_trace_log"
   val SIMP_TRACE_STEP = "simp_trace_step"
diff -r 5efff4075b63 -r 5c3484b90d5c src/Pure/Tools/simplifier_trace.ML
--- a/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 18:04:08 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 20:57:47 2014 +0200
@@ -60,36 +60,43 @@
      breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}: T
 )
 
-fun map_breakpoints f_term f_thm =
+val get_data = Data.get o Context.Proof
+val put_data = Context.proof_map o Data.put
+
+val get_breakpoints = #breakpoints o get_data
+
+fun map_breakpoints f =
   Data.map
-    (fn {max_depth, mode, interactive, parent, memory, breakpoints = (term_bs, thm_bs)} =>
+    (fn {max_depth, mode, interactive, parent, memory, breakpoints} =>
       {max_depth = max_depth,
        mode = mode,
        interactive = interactive,
        memory = memory,
        parent = parent,
-       breakpoints = (f_term term_bs, f_thm thm_bs)})
+       breakpoints = f breakpoints})
 
 fun add_term_breakpoint term =
-  map_breakpoints (Item_Net.update term) I
+  map_breakpoints (apfst (Item_Net.update term))
 
 fun add_thm_breakpoint thm context =
   let
     val rrules = mk_rrules (Context.proof_of context) [thm]
   in
-    map_breakpoints I (fold Item_Net.update rrules) context
+    map_breakpoints (apsnd (fold Item_Net.update rrules)) context
   end
 
-fun is_breakpoint (term, rrule) context =
+fun check_breakpoint (term, rrule) ctxt =
   let
-    val {breakpoints, ...} = Data.get context
+    val thy = Proof_Context.theory_of ctxt
+    val (term_bs, thm_bs) = get_breakpoints ctxt
 
-    fun matches pattern = Pattern.matches (Context.theory_of context) (pattern, term)
-    val term_matches = filter matches (Item_Net.retrieve_matching (fst breakpoints) term)
+    val term_matches =
+      filter (fn pat => Pattern.matches thy (pat, term))
+        (Item_Net.retrieve_matching term_bs term)
 
-    val {thm = thm, ...} = rrule
-    val thm_matches = exists (eq_rrule o pair rrule)
-      (Item_Net.retrieve_matching (snd breakpoints) (Thm.full_prop_of thm))
+    val thm_matches =
+      exists (eq_rrule o pair rrule)
+        (Item_Net.retrieve_matching thm_bs (Thm.full_prop_of (#thm rrule)))
   in
     (term_matches, thm_matches)
   end
@@ -146,7 +153,7 @@
 
 fun mk_generic_result markup text triggered (payload : unit -> payload) ctxt =
   let
-    val {mode, interactive, memory, parent, ...} = Data.get (Context.Proof ctxt)
+    val {mode, interactive, memory, parent, ...} = get_data ctxt
 
     val eligible =
       (case mode of
@@ -178,6 +185,14 @@
 
 (** tracing output **)
 
+fun see_panel () =
+  let
+    val ((bg1, bg2), en) =
+      YXML.output_markup_elem
+        (Active.make_markup Markup.simp_trace_panelN {implicit = false, properties = []})
+  in "See " ^ bg1 ^ bg2 ^ "simplifier trace" ^ en end
+
+
 fun send_request (result_id, content) =
   let
     fun break () =
@@ -195,7 +210,7 @@
 
 fun step ({term, thm, unconditional, ctxt, rrule}: data) =
   let
-    val (matching_terms, thm_triggered) = is_breakpoint (term, rrule) (Context.Proof ctxt)
+    val (matching_terms, thm_triggered) = check_breakpoint (term, rrule) ctxt
 
     val {name, ...} = rrule
     val term_triggered = not (null matching_terms)
@@ -232,21 +247,19 @@
         {props = [], pretty = pretty}
       end
 
-    val {max_depth, mode, interactive, memory, breakpoints, ...} =
-      Data.get (Context.Proof ctxt)
+    val {max_depth, mode, interactive, memory, breakpoints, ...} = get_data ctxt
 
     fun mk_promise result =
       let
         val result_id = #1 result
 
-        fun put mode' interactive' = Data.put
+        fun put mode' interactive' = put_data
           {max_depth = max_depth,
            mode = mode',
            interactive = interactive',
            memory = memory,
            parent = result_id,
-           breakpoints = breakpoints} (Context.Proof ctxt) |>
-          Context.the_proof
+           breakpoints = breakpoints} ctxt
 
         fun to_response "skip" = NONE
           | to_response "continue" = SOME (put mode true)
@@ -273,22 +286,23 @@
       {props = [],
        pretty = Syntax.pretty_term ctxt term}
 
-    val {max_depth, mode, interactive, memory, breakpoints, ...} =
-      Data.get (Context.Proof ctxt)
+    val {max_depth, mode, interactive, memory, breakpoints, ...} = get_data ctxt
 
-    fun put result_id = Data.put
+    fun put result_id = put_data
       {max_depth = max_depth,
        mode = if depth >= max_depth then Disabled else mode,
        interactive = interactive,
        memory = memory,
        parent = result_id,
-       breakpoints = breakpoints} (Context.Proof ctxt)
-
-    val context' =
-      (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of
-        NONE => put 0
-      | SOME res => (output_result res; put (#1 res)))
-  in Context.the_proof context' end
+       breakpoints = breakpoints} ctxt
+  in
+    (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of
+      NONE => put 0
+    | SOME res =>
+       (if depth = 1 then writeln (see_panel ()) else ();
+        output_result res;
+        put (#1 res)))
+  end
 
 fun indicate_failure ({term, ctxt, thm, rrule, ...}: data) ctxt' =
   let
@@ -314,7 +328,7 @@
         {props = [(successN, "false")], pretty = pretty}
       end
 
-    val {interactive, ...} = Data.get (Context.Proof ctxt)
+    val {interactive, ...} = get_data ctxt
 
     fun mk_promise result =
       let
@@ -419,7 +433,7 @@
   (Attrib.setup @{binding simp_break}
     (Scan.repeat Args.term_pattern >> breakpoint)
     "declaration of a simplifier breakpoint" #>
-   Attrib.setup @{binding simplifier_trace} (Scan.lift config_parser)
+   Attrib.setup @{binding simp_trace_new} (Scan.lift config_parser)
     "simplifier trace configuration")
 
 end
diff -r 5efff4075b63 -r 5c3484b90d5c src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Mon Jul 21 18:04:08 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala	Mon Jul 21 20:57:47 2014 +0200
@@ -65,7 +65,6 @@
       val continue_passive = Answer("continue_passive", "Continue (without asking)")
       val continue_disable = Answer("continue_disable", "Continue (without any trace)")
 
-      val default = skip
       val all = List(continue, continue_trace, continue_passive, continue_disable, skip)
     }
 
@@ -74,27 +73,12 @@
       val exit = Answer("exit", "Exit")
       val redo = Answer("redo", "Redo")
 
-      val default = exit
       val all = List(redo, exit)
     }
   }
 
   val all_answers: List[Answer] = Answer.step.all ::: Answer.hint_fail.all
 
-  object Active
-  {
-    def unapply(tree: XML.Tree): Option[(Long, Answer)] =
-      tree match {
-        case XML.Elem(Markup(Markup.SIMP_TRACE, props), _) =>
-          (props, props) match {
-            case (Markup.Serial(serial), Markup.Name(name)) =>
-              all_answers.find(_.name == name).map((serial, _))
-            case _ => None
-          }
-        case _ => None
-      }
-  }
-
 
   /* GUI interaction */
 
@@ -110,7 +94,7 @@
   private object Clear_Memory
   case class Reply(session: Session, serial: Long, answer: Answer)
 
-  case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer)
+  case class Question(data: Item.Data, answers: List[Answer])
 
   case class Context(
     last_serial: Long = 0L,
@@ -207,7 +191,7 @@
                         case Some(answer) if data.memory =>
                           do_reply(session, serial, answer)
                         case _ =>
-                          new_context += Question(data, Answer.step.all, Answer.step.default)
+                          new_context += Question(data, Answer.step.all)
                       }
 
                     case Markup.SIMP_TRACE_HINT =>
@@ -215,11 +199,10 @@
                         case Success(false) =>
                           results.get(data.parent) match {
                             case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
-                              new_context +=
-                                Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
+                              new_context += Question(data, Answer.hint_fail.all)
                             case _ =>
                               // unknown, better send a default reply
-                              do_reply(session, data.serial, Answer.hint_fail.default)
+                              do_reply(session, data.serial, Answer.hint_fail.exit)
                           }
                         case _ =>
                       }
@@ -263,8 +246,7 @@
             // current results.
 
             val items =
-              (for { (_, Item(_, data)) <- results.iterator }
-                yield data).toList
+              results.iterator.collect { case (_, Item(_, data)) => data }.toList
 
             slot.fulfill(Trace(items))
 
@@ -281,7 +263,7 @@
 
           case Reply(session, serial, answer) =>
             find_question(serial) match {
-              case Some((id, Question(data, _, _))) =>
+              case Some((id, Question(data, _))) =>
                 if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
                 {
                   val index = Index.of_data(data)
diff -r 5efff4075b63 -r 5c3484b90d5c src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Mon Jul 21 18:04:08 2014 +0200
+++ b/src/Tools/jEdit/src/active.scala	Mon Jul 21 20:57:47 2014 +0200
@@ -48,6 +48,11 @@
                   Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
                 }
 
+              case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, _), _) =>
+                Swing_Thread.later {
+                  view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
+                }
+
               case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
                 props match {
                   case Position.Id(id) =>
@@ -60,9 +65,6 @@
                 }
                 text_area.requestFocus
 
-              case Simplifier_Trace.Active(serial, answer) =>
-                Simplifier_Trace.send_reply(PIDE.session, serial, answer)
-
               case Protocol.Dialog(id, serial, result) =>
                 model.session.dialog_result(id, serial, result)
 
diff -r 5efff4075b63 -r 5c3484b90d5c src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Mon Jul 21 18:04:08 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Jul 21 20:57:47 2014 +0200
@@ -171,7 +171,7 @@
             line_text <- JEdit_Lib.try_get_text(buffer, line_range)
             result <-
               syntax.completion.complete(
-                history, decode, explicit, line_start, line_text, caret - line_start, false, context)
+                history, decode, explicit, line_start, line_text, caret - line_start, context)
           } yield result
 
         case None => None
@@ -558,7 +558,7 @@
 
           val context = syntax.language_context
 
-          syntax.completion.complete(history, true, false, 0, text, caret, false, context) match {
+          syntax.completion.complete(history, true, false, 0, text, caret, context) match {
             case Some(result) =>
               val fm = text_field.getFontMetrics(text_field.getFont)
               val loc =
diff -r 5efff4075b63 -r 5c3484b90d5c src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Jul 21 18:04:08 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Jul 21 20:57:47 2014 +0200
@@ -149,7 +149,7 @@
 
   private val active_elements =
     Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
-      Markup.SENDBACK, Markup.SIMP_TRACE)
+      Markup.SENDBACK, Markup.SIMP_TRACE_PANEL)
 
   private val tooltip_message_elements =
     Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
diff -r 5efff4075b63 -r 5c3484b90d5c src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Mon Jul 21 18:04:08 2014 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Mon Jul 21 20:57:47 2014 +0200
@@ -29,50 +29,38 @@
   private var current_results = Command.Results.empty
   private var current_id = 0L
   private var do_update = true
-  private var do_auto_reply = false
 
 
   private val text_area = new Pretty_Text_Area(view)
   set_content(text_area)
 
-  private def get_content(snapshot: Document.Snapshot, question: Simplifier_Trace.Question): XML.Tree =
+  private def update_contents()
   {
-    val data = question.data
 
-    def make_button(answer: Simplifier_Trace.Answer): XML.Tree =
-      XML.Wrapped_Elem(
-        Markup(Markup.SIMP_TRACE, Markup.Serial(data.serial) ::: Markup.Name(answer.name)),
-        Nil,
-        List(XML.Text(answer.string))
-      )
+    Swing_Thread.require {}
 
-    def make_block(body: XML.Body): XML.Body =
-      List(Pretty.Block(0, body))
+    val snapshot = current_snapshot
+    val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
 
-    val all = Pretty.separate(
-      XML.Text(data.text) ::
-      data.content :::
-      make_block(Library.separate(XML.Text(", "), question.answers map make_button))
-    )
-
-    XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(all)))
-  }
+    answers.contents.clear()
+    context.questions.values.toList match {
+      case q :: _ =>
+        val data = q.data
+        val content = Pretty.separate(XML.Text(data.text) :: data.content)
+        text_area.update(snapshot, Command.Results.empty, content)
+        q.answers.foreach { answer =>
+          answers.contents += new Button(answer.string) {
+            reactions += {
+              case ButtonClicked(_) =>
+                Simplifier_Trace.send_reply(PIDE.session, data.serial, answer)
+            }
+          }
+        }
+      case Nil =>
+        text_area.update(snapshot, Command.Results.empty, Nil)
+    }
 
-  private def set_context(snapshot: Document.Snapshot, context: Simplifier_Trace.Context)
-  {
-    Swing_Thread.require {}
-    val questions = context.questions.values
-    if (do_auto_reply && !questions.isEmpty)
-    {
-      questions.foreach(q => Simplifier_Trace.send_reply(PIDE.session, q.data.serial, q.default_answer))
-      handle_update(do_update)
-    }
-    else
-    {
-      val contents = Pretty.separate(questions.map(get_content(snapshot, _))(collection.breakOut))
-      text_area.update(snapshot, Command.Results.empty, contents)
-      do_paint()
-    }
+    do_paint()
   }
 
   private def show_trace()
@@ -88,14 +76,6 @@
     }
   }
 
-  private def update_contents()
-  {
-    set_context(
-      current_snapshot,
-      Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
-    )
-  }
-
   private def handle_resize()
   {
     do_paint()
@@ -195,15 +175,6 @@
       }
     },
     new Separator(Orientation.Vertical),
-    new CheckBox("Auto reply") {
-      selected = do_auto_reply
-      reactions += {
-        case ButtonClicked(_) =>
-          do_auto_reply = this.selected
-          handle_update(do_update)
-      }
-    },
-    new Separator(Orientation.Vertical),
     new Button("Show trace") {
       reactions += {
         case ButtonClicked(_) =>
@@ -218,5 +189,8 @@
     }
   )
 
+  private val answers = new Wrap_Panel(Wrap_Panel.Alignment.Left)()
+
   add(controls.peer, BorderLayout.NORTH)
+  add(answers.peer, BorderLayout.SOUTH)
 }