merged
authorwenzelm
Mon Jul 21 20:57:47 2014 +0200 (2014-07-21)
changeset 575975c3484b90d5c
parent 57586 5efff4075b63
parent 57596 3a1b1bda702f
child 57601 22e810680123
merged
     1.1 --- a/Admin/components/components.sha1	Mon Jul 21 18:04:08 2014 +0200
     1.2 +++ b/Admin/components/components.sha1	Mon Jul 21 20:57:47 2014 +0200
     1.3 @@ -26,6 +26,7 @@
     1.4  5080274f8721a18111a7f614793afe6c88726739  jdk-7u25.tar.gz
     1.5  dd24d63afd6d17b29ec9cb2b2464d4ff2e02de2c  jdk-7u40.tar.gz
     1.6  71b629b2ce83dbb69967c4785530afce1bec3809  jdk-7u60.tar.gz
     1.7 +e119f4cbfa2a39a53b9578d165d0dc44b59527b7  jdk-7u65.tar.gz
     1.8  ec740ee9ffd43551ddf1e5b91641405116af6291  jdk-7u6.tar.gz
     1.9  7d5b152ac70f720bb9e783fa45ecadcf95069584  jdk-7u9.tar.gz
    1.10  5442f1015a0657259be0590b04572cd933431df7  jdk-8u11.tar.gz
     2.1 --- a/Admin/components/main	Mon Jul 21 18:04:08 2014 +0200
     2.2 +++ b/Admin/components/main	Mon Jul 21 20:57:47 2014 +0200
     2.3 @@ -3,7 +3,7 @@
     2.4  e-1.8
     2.5  exec_process-1.0.3
     2.6  Haskabelle-2013
     2.7 -jdk-7u60
     2.8 +jdk-7u65
     2.9  jedit_build-20140511
    2.10  jfreechart-1.0.14-1
    2.11  jortho-1.0-2
     3.1 --- a/Admin/java/build	Mon Jul 21 18:04:08 2014 +0200
     3.2 +++ b/Admin/java/build	Mon Jul 21 20:57:47 2014 +0200
     3.3 @@ -11,8 +11,8 @@
     3.4  
     3.5  ## parameters
     3.6  
     3.7 -VERSION="8u11"
     3.8 -FULL_VERSION="1.8.0_11"
     3.9 +VERSION="7u65"
    3.10 +FULL_VERSION="1.7.0_65"
    3.11  
    3.12  ARCHIVE_LINUX32="jdk-${VERSION}-linux-i586.tar.gz"
    3.13  ARCHIVE_LINUX64="jdk-${VERSION}-linux-x64.tar.gz"
    3.14 @@ -113,7 +113,7 @@
    3.15      do
    3.16        if cmp -s "$FILE" "$OTHER"
    3.17        then
    3.18 -        echo -n "."
    3.19 +        echo -n "*"
    3.20          ln -f "$FILE" "$OTHER"
    3.21        fi
    3.22      done
     4.1 --- a/NEWS	Mon Jul 21 18:04:08 2014 +0200
     4.2 +++ b/NEWS	Mon Jul 21 20:57:47 2014 +0200
     4.3 @@ -116,7 +116,7 @@
     4.4  "Detach" a copy where this makes sense.
     4.5  
     4.6  * New Simplifier Trace panel provides an interactive view of the
     4.7 -simplification process, enabled by the "simplifier_trace" attribute
     4.8 +simplification process, enabled by the "simp_trace_new" attribute
     4.9  within the context.
    4.10  
    4.11  
     5.1 --- a/src/Doc/Isar_Ref/Generic.thy	Mon Jul 21 18:04:08 2014 +0200
     5.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Mon Jul 21 20:57:47 2014 +0200
     5.3 @@ -395,10 +395,12 @@
     5.4  subsection {* Simplification methods \label{sec:simp-meth} *}
     5.5  
     5.6  text {*
     5.7 -  \begin{matharray}{rcl}
     5.8 +  \begin{tabular}{rcll}
     5.9      @{method_def simp} & : & @{text method} \\
    5.10      @{method_def simp_all} & : & @{text method} \\
    5.11 -  \end{matharray}
    5.12 +    @{attribute_def simp_depth_limit} & : & @{text attribute} & default @{text 100} \\
    5.13 +  \end{tabular}
    5.14 +  \medskip
    5.15  
    5.16    @{rail \<open>
    5.17      (@@{method simp} | @@{method simp_all}) opt? (@{syntax simpmod} * )
    5.18 @@ -463,6 +465,9 @@
    5.19    The proof method fails if all subgoals remain unchanged after
    5.20    simplification.
    5.21  
    5.22 +  \item @{attribute simp_depth_limit} limits the number of recursive
    5.23 +  invocations of the Simplifier during conditional rewriting.
    5.24 +
    5.25    \end{description}
    5.26  
    5.27    By default the Simplifier methods above take local assumptions fully
    5.28 @@ -586,7 +591,7 @@
    5.29    apply simp
    5.30    oops
    5.31  
    5.32 -text {* See also \secref{sec:simp-config} for options to enable
    5.33 +text {* See also \secref{sec:simp-trace} for options to enable
    5.34    Simplifier trace mode, which often helps to diagnose problems with
    5.35    rewrite systems.
    5.36  *}
    5.37 @@ -859,25 +864,32 @@
    5.38    reorientation and mutual simplification fail to apply.  *}
    5.39  
    5.40  
    5.41 -subsection {* Configuration options \label{sec:simp-config} *}
    5.42 +subsection {* Simplifier tracing and debugging \label{sec:simp-trace} *}
    5.43  
    5.44  text {*
    5.45    \begin{tabular}{rcll}
    5.46 -    @{attribute_def simp_depth_limit} & : & @{text attribute} & default @{text 100} \\
    5.47      @{attribute_def simp_trace} & : & @{text attribute} & default @{text false} \\
    5.48      @{attribute_def simp_trace_depth_limit} & : & @{text attribute} & default @{text 1} \\
    5.49      @{attribute_def simp_debug} & : & @{text attribute} & default @{text false} \\
    5.50 +    @{attribute_def simp_trace_new} & : & @{text attribute} \\
    5.51 +    @{attribute_def simp_break} & : & @{text attribute} \\
    5.52    \end{tabular}
    5.53    \medskip
    5.54  
    5.55 -  These configurations options control further aspects of the Simplifier.
    5.56 -  See also \secref{sec:config}.
    5.57 +  @{rail \<open>
    5.58 +    @@{attribute simp_trace_new} ('interactive')? \<newline>
    5.59 +      ('mode' '=' ('full' | 'normal'))? \<newline>
    5.60 +      ('depth' '=' @{syntax nat})?
    5.61 +    ;
    5.62 +
    5.63 +    @@{attribute simp_break} (@{syntax term}*)
    5.64 +  \<close>}
    5.65 +
    5.66 +  These attributes and configurations options control various aspects of
    5.67 +  Simplifier tracing and debugging.
    5.68  
    5.69    \begin{description}
    5.70  
    5.71 -  \item @{attribute simp_depth_limit} limits the number of recursive
    5.72 -  invocations of the Simplifier during conditional rewriting.
    5.73 -
    5.74    \item @{attribute simp_trace} makes the Simplifier output internal
    5.75    operations.  This includes rewrite steps, but also bookkeeping like
    5.76    modifications of the simpset.
    5.77 @@ -890,9 +902,30 @@
    5.78    information about internal operations.  This includes any attempted
    5.79    invocation of simplification procedures.
    5.80  
    5.81 +  \item @{attribute simp_trace_new} controls Simplifier tracing within
    5.82 +  Isabelle/PIDE applications, notably Isabelle/jEdit \cite{isabelle-jedit}.
    5.83 +  This provides a hierarchical representation of the rewriting steps
    5.84 +  performed by the Simplifier.
    5.85 +
    5.86 +  Users can configure the behaviour by specifying breakpoints, verbosity and
    5.87 +  enabling or disabling the interactive mode. In normal verbosity (the
    5.88 +  default), only rule applications matching a breakpoint will be shown to
    5.89 +  the user. In full verbosity, all rule applications will be logged.
    5.90 +  Interactive mode interrupts the normal flow of the Simplifier and defers
    5.91 +  the decision how to continue to the user via some GUI dialog.
    5.92 +
    5.93 +  \item @{attribute simp_break} declares term or theorem breakpoints for
    5.94 +  @{attribute simp_trace_new} as described above. Term breakpoints are
    5.95 +  patterns which are checked for matches on the redex of a rule application.
    5.96 +  Theorem breakpoints trigger when the corresponding theorem is applied in a
    5.97 +  rewrite step. For example:
    5.98 +
    5.99    \end{description}
   5.100  *}
   5.101  
   5.102 +declare conjI [simp_break]
   5.103 +declare [[simp_break "?x \<and> ?y"]]
   5.104 +
   5.105  
   5.106  subsection {* Simplification procedures \label{sec:simproc} *}
   5.107  
     6.1 --- a/src/Doc/Isar_Ref/document/root.tex	Mon Jul 21 18:04:08 2014 +0200
     6.2 +++ b/src/Doc/Isar_Ref/document/root.tex	Mon Jul 21 20:57:47 2014 +0200
     6.3 @@ -34,14 +34,15 @@
     6.4    Lucas Dixon,
     6.5    Florian Haftmann, \\
     6.6    Brian Huffman,
     6.7 -  Gerwin Klein,
     6.8 -  Alexander Krauss, \\
     6.9 +  Lars Hupel,
    6.10 +  Gerwin Klein, \\
    6.11 +  Alexander Krauss,
    6.12    Ond\v{r}ej Kun\v{c}ar,
    6.13 -  Andreas Lochbihler,
    6.14 -  Tobias Nipkow, \\
    6.15 +  Andreas Lochbihler, \\
    6.16 +  Tobias Nipkow,
    6.17    Lars Noschinski,
    6.18 -  David von Oheimb,
    6.19 -  Larry Paulson, \\
    6.20 +  David von Oheimb, \\
    6.21 +  Larry Paulson,
    6.22    Sebastian Skalberg,
    6.23    Christian Sternagel
    6.24  }
     7.1 --- a/src/Doc/JEdit/JEdit.thy	Mon Jul 21 18:04:08 2014 +0200
     7.2 +++ b/src/Doc/JEdit/JEdit.thy	Mon Jul 21 20:57:47 2014 +0200
     7.3 @@ -1225,6 +1225,12 @@
     7.4    situations, to tell that some language keywords should be excluded from
     7.5    further completion attempts. For example, @{verbatim ":"} within accepted
     7.6    Isar syntax looses its meaning as abbreviation for symbol @{text "\<in>"}.
     7.7 +
     7.8 +  \medskip The completion context is \emph{ignored} for built-in templates and
     7.9 +  symbols in their explicit form ``@{verbatim "\<foobar>"}''; see also
    7.10 +  \secref{sec:completion-varieties}. This allows to complete within broken
    7.11 +  input that escapes its normal semantic context, e.g.\ antiquotations or
    7.12 +  string literals in ML, which do not allow arbitrary backslash sequences.
    7.13  *}
    7.14  
    7.15  
     8.1 --- a/src/Pure/General/completion.scala	Mon Jul 21 18:04:08 2014 +0200
     8.2 +++ b/src/Pure/General/completion.scala	Mon Jul 21 20:57:47 2014 +0200
     8.3 @@ -11,6 +11,7 @@
     8.4  
     8.5  import scala.collection.immutable.SortedMap
     8.6  import scala.util.parsing.combinator.RegexParsers
     8.7 +import scala.util.matching.Regex
     8.8  import scala.math.Ordering
     8.9  
    8.10  
    8.11 @@ -219,6 +220,9 @@
    8.12    {
    8.13      override val whiteSpace = "".r
    8.14  
    8.15 +    private val symbol_regex: Regex = """\\<\^?[A-Za-z0-9_']+>""".r
    8.16 +    def is_symbol(s: CharSequence): Boolean = symbol_regex.pattern.matcher(s).matches
    8.17 +
    8.18      private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
    8.19      private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
    8.20      private def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
    8.21 @@ -231,16 +235,6 @@
    8.22      def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
    8.23      def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.'
    8.24  
    8.25 -    def extend_word(text: CharSequence, offset: Text.Offset): Text.Offset =
    8.26 -    {
    8.27 -      val n = text.length
    8.28 -      var i = offset
    8.29 -      while (i < n && is_word_char(text.charAt(i))) i += 1
    8.30 -      if (i < n && text.charAt(i) == '>' && read_symbol(text.subSequence(0, i + 1)).isDefined)
    8.31 -        i + 1
    8.32 -      else i
    8.33 -    }
    8.34 -
    8.35      def read_symbol(in: CharSequence): Option[String] =
    8.36      {
    8.37        val reverse_in = new Library.Reverse(in)
    8.38 @@ -341,7 +335,6 @@
    8.39      start: Text.Offset,
    8.40      text: CharSequence,
    8.41      caret: Int,
    8.42 -    extend_word: Boolean,
    8.43      language_context: Completion.Language_Context): Option[Completion.Result] =
    8.44    {
    8.45      def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
    8.46 @@ -358,8 +351,11 @@
    8.47              case (a, _) :: _ =>
    8.48                val ok =
    8.49                  if (a == Completion.antiquote) language_context.antiquotes
    8.50 -                else language_context.symbols || Completion.default_abbrs.exists(_._1 == a)
    8.51 -              if (ok) Some(((a, abbrevs), caret))
    8.52 +                else
    8.53 +                  language_context.symbols ||
    8.54 +                  Completion.default_abbrs.exists(_._1 == a) ||
    8.55 +                  Completion.Word_Parsers.is_symbol(a)
    8.56 +              if (ok) Some((a, abbrevs))
    8.57                else None
    8.58            }
    8.59          case _ => None
    8.60 @@ -369,17 +365,10 @@
    8.61      val words_result =
    8.62        if (abbrevs_result.isDefined) None
    8.63        else {
    8.64 -        val end =
    8.65 -          if (extend_word) Completion.Word_Parsers.extend_word(text, caret)
    8.66 -          else caret
    8.67          val result =
    8.68 -          Completion.Word_Parsers.read_symbol(text.subSequence(0, end)) match {
    8.69 +          Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match {
    8.70              case Some(symbol) => Some((symbol, ""))
    8.71 -            case None =>
    8.72 -              val word_context =
    8.73 -                end < length && Completion.Word_Parsers.is_word_char(text.charAt(end))
    8.74 -              if (word_context) None
    8.75 -              else Completion.Word_Parsers.read_word(explicit, text.subSequence(0, end))
    8.76 +            case None => Completion.Word_Parsers.read_word(explicit, text.subSequence(0, caret))
    8.77            }
    8.78          result.map(
    8.79            {
    8.80 @@ -397,13 +386,13 @@
    8.81                      if ok
    8.82                      completion <- words_map.get_list(complete_word)
    8.83                    } yield (complete_word, completion)
    8.84 -              (((full_word, completions), end))
    8.85 +              ((full_word, completions))
    8.86            })
    8.87        }
    8.88  
    8.89      (abbrevs_result orElse words_result) match {
    8.90 -      case Some(((original, completions), end)) if !completions.isEmpty =>
    8.91 -        val range = Text.Range(- original.length, 0) + end + start
    8.92 +      case Some((original, completions)) if !completions.isEmpty =>
    8.93 +        val range = Text.Range(- original.length, 0) + caret + start
    8.94          val immediate =
    8.95            explicit ||
    8.96              (!Completion.Word_Parsers.is_word(original) &&
     9.1 --- a/src/Pure/PIDE/markup.ML	Mon Jul 21 18:04:08 2014 +0200
     9.2 +++ b/src/Pure/PIDE/markup.ML	Mon Jul 21 20:57:47 2014 +0200
     9.3 @@ -185,6 +185,7 @@
     9.4    val use_theories_result: string -> bool -> Properties.T
     9.5    val print_operationsN: string
     9.6    val print_operations: Properties.T
     9.7 +  val simp_trace_panelN: string
     9.8    val simp_trace_logN: string
     9.9    val simp_trace_stepN: string
    9.10    val simp_trace_recurseN: string
    9.11 @@ -586,6 +587,8 @@
    9.12  
    9.13  (* simplifier trace *)
    9.14  
    9.15 +val simp_trace_panelN = "simp_trace_panel";
    9.16 +
    9.17  val simp_trace_logN = "simp_trace_log";
    9.18  val simp_trace_stepN = "simp_trace_step";
    9.19  val simp_trace_recurseN = "simp_trace_recurse";
    10.1 --- a/src/Pure/PIDE/markup.scala	Mon Jul 21 18:04:08 2014 +0200
    10.2 +++ b/src/Pure/PIDE/markup.scala	Mon Jul 21 20:57:47 2014 +0200
    10.3 @@ -464,7 +464,7 @@
    10.4  
    10.5    /* simplifier trace */
    10.6  
    10.7 -  val SIMP_TRACE = "simp_trace"
    10.8 +  val SIMP_TRACE_PANEL = "simp_trace_panel"
    10.9  
   10.10    val SIMP_TRACE_LOG = "simp_trace_log"
   10.11    val SIMP_TRACE_STEP = "simp_trace_step"
    11.1 --- a/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 18:04:08 2014 +0200
    11.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 20:57:47 2014 +0200
    11.3 @@ -60,36 +60,43 @@
    11.4       breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}: T
    11.5  )
    11.6  
    11.7 -fun map_breakpoints f_term f_thm =
    11.8 +val get_data = Data.get o Context.Proof
    11.9 +val put_data = Context.proof_map o Data.put
   11.10 +
   11.11 +val get_breakpoints = #breakpoints o get_data
   11.12 +
   11.13 +fun map_breakpoints f =
   11.14    Data.map
   11.15 -    (fn {max_depth, mode, interactive, parent, memory, breakpoints = (term_bs, thm_bs)} =>
   11.16 +    (fn {max_depth, mode, interactive, parent, memory, breakpoints} =>
   11.17        {max_depth = max_depth,
   11.18         mode = mode,
   11.19         interactive = interactive,
   11.20         memory = memory,
   11.21         parent = parent,
   11.22 -       breakpoints = (f_term term_bs, f_thm thm_bs)})
   11.23 +       breakpoints = f breakpoints})
   11.24  
   11.25  fun add_term_breakpoint term =
   11.26 -  map_breakpoints (Item_Net.update term) I
   11.27 +  map_breakpoints (apfst (Item_Net.update term))
   11.28  
   11.29  fun add_thm_breakpoint thm context =
   11.30    let
   11.31      val rrules = mk_rrules (Context.proof_of context) [thm]
   11.32    in
   11.33 -    map_breakpoints I (fold Item_Net.update rrules) context
   11.34 +    map_breakpoints (apsnd (fold Item_Net.update rrules)) context
   11.35    end
   11.36  
   11.37 -fun is_breakpoint (term, rrule) context =
   11.38 +fun check_breakpoint (term, rrule) ctxt =
   11.39    let
   11.40 -    val {breakpoints, ...} = Data.get context
   11.41 +    val thy = Proof_Context.theory_of ctxt
   11.42 +    val (term_bs, thm_bs) = get_breakpoints ctxt
   11.43  
   11.44 -    fun matches pattern = Pattern.matches (Context.theory_of context) (pattern, term)
   11.45 -    val term_matches = filter matches (Item_Net.retrieve_matching (fst breakpoints) term)
   11.46 +    val term_matches =
   11.47 +      filter (fn pat => Pattern.matches thy (pat, term))
   11.48 +        (Item_Net.retrieve_matching term_bs term)
   11.49  
   11.50 -    val {thm = thm, ...} = rrule
   11.51 -    val thm_matches = exists (eq_rrule o pair rrule)
   11.52 -      (Item_Net.retrieve_matching (snd breakpoints) (Thm.full_prop_of thm))
   11.53 +    val thm_matches =
   11.54 +      exists (eq_rrule o pair rrule)
   11.55 +        (Item_Net.retrieve_matching thm_bs (Thm.full_prop_of (#thm rrule)))
   11.56    in
   11.57      (term_matches, thm_matches)
   11.58    end
   11.59 @@ -146,7 +153,7 @@
   11.60  
   11.61  fun mk_generic_result markup text triggered (payload : unit -> payload) ctxt =
   11.62    let
   11.63 -    val {mode, interactive, memory, parent, ...} = Data.get (Context.Proof ctxt)
   11.64 +    val {mode, interactive, memory, parent, ...} = get_data ctxt
   11.65  
   11.66      val eligible =
   11.67        (case mode of
   11.68 @@ -178,6 +185,14 @@
   11.69  
   11.70  (** tracing output **)
   11.71  
   11.72 +fun see_panel () =
   11.73 +  let
   11.74 +    val ((bg1, bg2), en) =
   11.75 +      YXML.output_markup_elem
   11.76 +        (Active.make_markup Markup.simp_trace_panelN {implicit = false, properties = []})
   11.77 +  in "See " ^ bg1 ^ bg2 ^ "simplifier trace" ^ en end
   11.78 +
   11.79 +
   11.80  fun send_request (result_id, content) =
   11.81    let
   11.82      fun break () =
   11.83 @@ -195,7 +210,7 @@
   11.84  
   11.85  fun step ({term, thm, unconditional, ctxt, rrule}: data) =
   11.86    let
   11.87 -    val (matching_terms, thm_triggered) = is_breakpoint (term, rrule) (Context.Proof ctxt)
   11.88 +    val (matching_terms, thm_triggered) = check_breakpoint (term, rrule) ctxt
   11.89  
   11.90      val {name, ...} = rrule
   11.91      val term_triggered = not (null matching_terms)
   11.92 @@ -232,21 +247,19 @@
   11.93          {props = [], pretty = pretty}
   11.94        end
   11.95  
   11.96 -    val {max_depth, mode, interactive, memory, breakpoints, ...} =
   11.97 -      Data.get (Context.Proof ctxt)
   11.98 +    val {max_depth, mode, interactive, memory, breakpoints, ...} = get_data ctxt
   11.99  
  11.100      fun mk_promise result =
  11.101        let
  11.102          val result_id = #1 result
  11.103  
  11.104 -        fun put mode' interactive' = Data.put
  11.105 +        fun put mode' interactive' = put_data
  11.106            {max_depth = max_depth,
  11.107             mode = mode',
  11.108             interactive = interactive',
  11.109             memory = memory,
  11.110             parent = result_id,
  11.111 -           breakpoints = breakpoints} (Context.Proof ctxt) |>
  11.112 -          Context.the_proof
  11.113 +           breakpoints = breakpoints} ctxt
  11.114  
  11.115          fun to_response "skip" = NONE
  11.116            | to_response "continue" = SOME (put mode true)
  11.117 @@ -273,22 +286,23 @@
  11.118        {props = [],
  11.119         pretty = Syntax.pretty_term ctxt term}
  11.120  
  11.121 -    val {max_depth, mode, interactive, memory, breakpoints, ...} =
  11.122 -      Data.get (Context.Proof ctxt)
  11.123 +    val {max_depth, mode, interactive, memory, breakpoints, ...} = get_data ctxt
  11.124  
  11.125 -    fun put result_id = Data.put
  11.126 +    fun put result_id = put_data
  11.127        {max_depth = max_depth,
  11.128         mode = if depth >= max_depth then Disabled else mode,
  11.129         interactive = interactive,
  11.130         memory = memory,
  11.131         parent = result_id,
  11.132 -       breakpoints = breakpoints} (Context.Proof ctxt)
  11.133 -
  11.134 -    val context' =
  11.135 -      (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of
  11.136 -        NONE => put 0
  11.137 -      | SOME res => (output_result res; put (#1 res)))
  11.138 -  in Context.the_proof context' end
  11.139 +       breakpoints = breakpoints} ctxt
  11.140 +  in
  11.141 +    (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of
  11.142 +      NONE => put 0
  11.143 +    | SOME res =>
  11.144 +       (if depth = 1 then writeln (see_panel ()) else ();
  11.145 +        output_result res;
  11.146 +        put (#1 res)))
  11.147 +  end
  11.148  
  11.149  fun indicate_failure ({term, ctxt, thm, rrule, ...}: data) ctxt' =
  11.150    let
  11.151 @@ -314,7 +328,7 @@
  11.152          {props = [(successN, "false")], pretty = pretty}
  11.153        end
  11.154  
  11.155 -    val {interactive, ...} = Data.get (Context.Proof ctxt)
  11.156 +    val {interactive, ...} = get_data ctxt
  11.157  
  11.158      fun mk_promise result =
  11.159        let
  11.160 @@ -419,7 +433,7 @@
  11.161    (Attrib.setup @{binding simp_break}
  11.162      (Scan.repeat Args.term_pattern >> breakpoint)
  11.163      "declaration of a simplifier breakpoint" #>
  11.164 -   Attrib.setup @{binding simplifier_trace} (Scan.lift config_parser)
  11.165 +   Attrib.setup @{binding simp_trace_new} (Scan.lift config_parser)
  11.166      "simplifier trace configuration")
  11.167  
  11.168  end
    12.1 --- a/src/Pure/Tools/simplifier_trace.scala	Mon Jul 21 18:04:08 2014 +0200
    12.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Mon Jul 21 20:57:47 2014 +0200
    12.3 @@ -65,7 +65,6 @@
    12.4        val continue_passive = Answer("continue_passive", "Continue (without asking)")
    12.5        val continue_disable = Answer("continue_disable", "Continue (without any trace)")
    12.6  
    12.7 -      val default = skip
    12.8        val all = List(continue, continue_trace, continue_passive, continue_disable, skip)
    12.9      }
   12.10  
   12.11 @@ -74,27 +73,12 @@
   12.12        val exit = Answer("exit", "Exit")
   12.13        val redo = Answer("redo", "Redo")
   12.14  
   12.15 -      val default = exit
   12.16        val all = List(redo, exit)
   12.17      }
   12.18    }
   12.19  
   12.20    val all_answers: List[Answer] = Answer.step.all ::: Answer.hint_fail.all
   12.21  
   12.22 -  object Active
   12.23 -  {
   12.24 -    def unapply(tree: XML.Tree): Option[(Long, Answer)] =
   12.25 -      tree match {
   12.26 -        case XML.Elem(Markup(Markup.SIMP_TRACE, props), _) =>
   12.27 -          (props, props) match {
   12.28 -            case (Markup.Serial(serial), Markup.Name(name)) =>
   12.29 -              all_answers.find(_.name == name).map((serial, _))
   12.30 -            case _ => None
   12.31 -          }
   12.32 -        case _ => None
   12.33 -      }
   12.34 -  }
   12.35 -
   12.36  
   12.37    /* GUI interaction */
   12.38  
   12.39 @@ -110,7 +94,7 @@
   12.40    private object Clear_Memory
   12.41    case class Reply(session: Session, serial: Long, answer: Answer)
   12.42  
   12.43 -  case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer)
   12.44 +  case class Question(data: Item.Data, answers: List[Answer])
   12.45  
   12.46    case class Context(
   12.47      last_serial: Long = 0L,
   12.48 @@ -207,7 +191,7 @@
   12.49                          case Some(answer) if data.memory =>
   12.50                            do_reply(session, serial, answer)
   12.51                          case _ =>
   12.52 -                          new_context += Question(data, Answer.step.all, Answer.step.default)
   12.53 +                          new_context += Question(data, Answer.step.all)
   12.54                        }
   12.55  
   12.56                      case Markup.SIMP_TRACE_HINT =>
   12.57 @@ -215,11 +199,10 @@
   12.58                          case Success(false) =>
   12.59                            results.get(data.parent) match {
   12.60                              case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
   12.61 -                              new_context +=
   12.62 -                                Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
   12.63 +                              new_context += Question(data, Answer.hint_fail.all)
   12.64                              case _ =>
   12.65                                // unknown, better send a default reply
   12.66 -                              do_reply(session, data.serial, Answer.hint_fail.default)
   12.67 +                              do_reply(session, data.serial, Answer.hint_fail.exit)
   12.68                            }
   12.69                          case _ =>
   12.70                        }
   12.71 @@ -263,8 +246,7 @@
   12.72              // current results.
   12.73  
   12.74              val items =
   12.75 -              (for { (_, Item(_, data)) <- results.iterator }
   12.76 -                yield data).toList
   12.77 +              results.iterator.collect { case (_, Item(_, data)) => data }.toList
   12.78  
   12.79              slot.fulfill(Trace(items))
   12.80  
   12.81 @@ -281,7 +263,7 @@
   12.82  
   12.83            case Reply(session, serial, answer) =>
   12.84              find_question(serial) match {
   12.85 -              case Some((id, Question(data, _, _))) =>
   12.86 +              case Some((id, Question(data, _))) =>
   12.87                  if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
   12.88                  {
   12.89                    val index = Index.of_data(data)
    13.1 --- a/src/Tools/jEdit/src/active.scala	Mon Jul 21 18:04:08 2014 +0200
    13.2 +++ b/src/Tools/jEdit/src/active.scala	Mon Jul 21 20:57:47 2014 +0200
    13.3 @@ -48,6 +48,11 @@
    13.4                    Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
    13.5                  }
    13.6  
    13.7 +              case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, _), _) =>
    13.8 +                Swing_Thread.later {
    13.9 +                  view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
   13.10 +                }
   13.11 +
   13.12                case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
   13.13                  props match {
   13.14                    case Position.Id(id) =>
   13.15 @@ -60,9 +65,6 @@
   13.16                  }
   13.17                  text_area.requestFocus
   13.18  
   13.19 -              case Simplifier_Trace.Active(serial, answer) =>
   13.20 -                Simplifier_Trace.send_reply(PIDE.session, serial, answer)
   13.21 -
   13.22                case Protocol.Dialog(id, serial, result) =>
   13.23                  model.session.dialog_result(id, serial, result)
   13.24  
    14.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Mon Jul 21 18:04:08 2014 +0200
    14.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Jul 21 20:57:47 2014 +0200
    14.3 @@ -171,7 +171,7 @@
    14.4              line_text <- JEdit_Lib.try_get_text(buffer, line_range)
    14.5              result <-
    14.6                syntax.completion.complete(
    14.7 -                history, decode, explicit, line_start, line_text, caret - line_start, false, context)
    14.8 +                history, decode, explicit, line_start, line_text, caret - line_start, context)
    14.9            } yield result
   14.10  
   14.11          case None => None
   14.12 @@ -558,7 +558,7 @@
   14.13  
   14.14            val context = syntax.language_context
   14.15  
   14.16 -          syntax.completion.complete(history, true, false, 0, text, caret, false, context) match {
   14.17 +          syntax.completion.complete(history, true, false, 0, text, caret, context) match {
   14.18              case Some(result) =>
   14.19                val fm = text_field.getFontMetrics(text_field.getFont)
   14.20                val loc =
    15.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Jul 21 18:04:08 2014 +0200
    15.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Jul 21 20:57:47 2014 +0200
    15.3 @@ -149,7 +149,7 @@
    15.4  
    15.5    private val active_elements =
    15.6      Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    15.7 -      Markup.SENDBACK, Markup.SIMP_TRACE)
    15.8 +      Markup.SENDBACK, Markup.SIMP_TRACE_PANEL)
    15.9  
   15.10    private val tooltip_message_elements =
   15.11      Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
    16.1 --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Mon Jul 21 18:04:08 2014 +0200
    16.2 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Mon Jul 21 20:57:47 2014 +0200
    16.3 @@ -29,50 +29,38 @@
    16.4    private var current_results = Command.Results.empty
    16.5    private var current_id = 0L
    16.6    private var do_update = true
    16.7 -  private var do_auto_reply = false
    16.8  
    16.9  
   16.10    private val text_area = new Pretty_Text_Area(view)
   16.11    set_content(text_area)
   16.12  
   16.13 -  private def get_content(snapshot: Document.Snapshot, question: Simplifier_Trace.Question): XML.Tree =
   16.14 +  private def update_contents()
   16.15    {
   16.16 -    val data = question.data
   16.17  
   16.18 -    def make_button(answer: Simplifier_Trace.Answer): XML.Tree =
   16.19 -      XML.Wrapped_Elem(
   16.20 -        Markup(Markup.SIMP_TRACE, Markup.Serial(data.serial) ::: Markup.Name(answer.name)),
   16.21 -        Nil,
   16.22 -        List(XML.Text(answer.string))
   16.23 -      )
   16.24 +    Swing_Thread.require {}
   16.25  
   16.26 -    def make_block(body: XML.Body): XML.Body =
   16.27 -      List(Pretty.Block(0, body))
   16.28 +    val snapshot = current_snapshot
   16.29 +    val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
   16.30  
   16.31 -    val all = Pretty.separate(
   16.32 -      XML.Text(data.text) ::
   16.33 -      data.content :::
   16.34 -      make_block(Library.separate(XML.Text(", "), question.answers map make_button))
   16.35 -    )
   16.36 -
   16.37 -    XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(all)))
   16.38 -  }
   16.39 +    answers.contents.clear()
   16.40 +    context.questions.values.toList match {
   16.41 +      case q :: _ =>
   16.42 +        val data = q.data
   16.43 +        val content = Pretty.separate(XML.Text(data.text) :: data.content)
   16.44 +        text_area.update(snapshot, Command.Results.empty, content)
   16.45 +        q.answers.foreach { answer =>
   16.46 +          answers.contents += new Button(answer.string) {
   16.47 +            reactions += {
   16.48 +              case ButtonClicked(_) =>
   16.49 +                Simplifier_Trace.send_reply(PIDE.session, data.serial, answer)
   16.50 +            }
   16.51 +          }
   16.52 +        }
   16.53 +      case Nil =>
   16.54 +        text_area.update(snapshot, Command.Results.empty, Nil)
   16.55 +    }
   16.56  
   16.57 -  private def set_context(snapshot: Document.Snapshot, context: Simplifier_Trace.Context)
   16.58 -  {
   16.59 -    Swing_Thread.require {}
   16.60 -    val questions = context.questions.values
   16.61 -    if (do_auto_reply && !questions.isEmpty)
   16.62 -    {
   16.63 -      questions.foreach(q => Simplifier_Trace.send_reply(PIDE.session, q.data.serial, q.default_answer))
   16.64 -      handle_update(do_update)
   16.65 -    }
   16.66 -    else
   16.67 -    {
   16.68 -      val contents = Pretty.separate(questions.map(get_content(snapshot, _))(collection.breakOut))
   16.69 -      text_area.update(snapshot, Command.Results.empty, contents)
   16.70 -      do_paint()
   16.71 -    }
   16.72 +    do_paint()
   16.73    }
   16.74  
   16.75    private def show_trace()
   16.76 @@ -88,14 +76,6 @@
   16.77      }
   16.78    }
   16.79  
   16.80 -  private def update_contents()
   16.81 -  {
   16.82 -    set_context(
   16.83 -      current_snapshot,
   16.84 -      Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
   16.85 -    )
   16.86 -  }
   16.87 -
   16.88    private def handle_resize()
   16.89    {
   16.90      do_paint()
   16.91 @@ -195,15 +175,6 @@
   16.92        }
   16.93      },
   16.94      new Separator(Orientation.Vertical),
   16.95 -    new CheckBox("Auto reply") {
   16.96 -      selected = do_auto_reply
   16.97 -      reactions += {
   16.98 -        case ButtonClicked(_) =>
   16.99 -          do_auto_reply = this.selected
  16.100 -          handle_update(do_update)
  16.101 -      }
  16.102 -    },
  16.103 -    new Separator(Orientation.Vertical),
  16.104      new Button("Show trace") {
  16.105        reactions += {
  16.106          case ButtonClicked(_) =>
  16.107 @@ -218,5 +189,8 @@
  16.108      }
  16.109    )
  16.110  
  16.111 +  private val answers = new Wrap_Panel(Wrap_Panel.Alignment.Left)()
  16.112 +
  16.113    add(controls.peer, BorderLayout.NORTH)
  16.114 +  add(answers.peer, BorderLayout.SOUTH)
  16.115  }