--- 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
--- 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
--- 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
--- 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.
--- 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} *}
--- 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
}
--- 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.
*}
--- 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) &&
--- 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";
--- 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"
--- 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
--- 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)
--- 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)
--- 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 =
--- 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)
--- 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)
}