merged
authorAndreas Lochbihler
Tue Jul 22 08:07:47 2014 +0200 (2014-07-22)
changeset 5760122e810680123
parent 57600 b0ad484b7d1c
parent 57597 5c3484b90d5c
child 57602 0f708666eb7c
merged
     1.1 --- a/Admin/components/components.sha1	Mon Jul 21 17:57:16 2014 +0200
     1.2 +++ b/Admin/components/components.sha1	Tue Jul 22 08:07: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 17:57:16 2014 +0200
     2.2 +++ b/Admin/components/main	Tue Jul 22 08:07: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 17:57:16 2014 +0200
     3.2 +++ b/Admin/java/build	Tue Jul 22 08:07: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 17:57:16 2014 +0200
     4.2 +++ b/NEWS	Tue Jul 22 08:07: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 17:57:16 2014 +0200
     5.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Tue Jul 22 08:07: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 17:57:16 2014 +0200
     6.2 +++ b/src/Doc/Isar_Ref/document/root.tex	Tue Jul 22 08:07: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 17:57:16 2014 +0200
     7.2 +++ b/src/Doc/JEdit/JEdit.thy	Tue Jul 22 08:07: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 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/BNF_Examples/IsaFoR_Datatypes.thy	Tue Jul 22 08:07:47 2014 +0200
     8.3 @@ -0,0 +1,380 @@
     8.4 +(*  Title:      HOL/BNF_Examples/IsaFoR_Datatypes.thy
     8.5 +    Author:     René Thiemann
     8.6 +    Copyright   2014
     8.7 +
     8.8 +Benchmark of datatypes defined in IsaFoR
     8.9 +*)
    8.10 +
    8.11 +theory IsaFoR_Datatypes
    8.12 +imports
    8.13 +  Real
    8.14 +begin
    8.15 +
    8.16 +datatype_new ('f, 'l) lab =
    8.17 +  Lab "('f, 'l) lab" 'l
    8.18 +| FunLab "('f, 'l) lab" "('f, 'l) lab list"
    8.19 +| UnLab 'f
    8.20 +| Sharp "('f, 'l) lab"
    8.21 +
    8.22 +datatype_new 'f projL = Projection "(('f \<times> nat) \<times> nat) list"
    8.23 +
    8.24 +datatype_new ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list"
    8.25 +datatype_new ('f, 'v) ctxt =
    8.26 +  Hole ("\<box>")
    8.27 +| More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list"
    8.28 +
    8.29 +
    8.30 +type_synonym ('f, 'v) rule = "('f, 'v) term \<times> ('f, 'v) term"
    8.31 +type_synonym ('f, 'v) trs  = "('f, 'v) rule set"
    8.32 +
    8.33 +type_synonym ('f, 'v) rules = "('f,'v) rule list"
    8.34 +type_synonym ('f, 'l, 'v) ruleLL  = "(('f, 'l) lab, 'v) rule"
    8.35 +type_synonym ('f, 'l, 'v) trsLL   = "(('f, 'l) lab, 'v) rules"
    8.36 +type_synonym ('f, 'l, 'v) termsLL = "(('f, 'l) lab, 'v) term list"
    8.37 +datatype_new pos = Empty ("\<epsilon>") | PCons "nat" "pos" (infixr "<#" 70)
    8.38 +type_synonym  ('f, 'v) prseq = "(pos \<times> ('f, 'v) rule \<times> bool \<times> ('f, 'v) term) list"
    8.39 +type_synonym  ('f, 'v) rseq = "(pos \<times> ('f, 'v) rule \<times> ('f, 'v) term) list"
    8.40 +
    8.41 +type_synonym ('f, 'l, 'v) rseqL   = "((('f, 'l) lab, 'v) rule \<times> (('f, 'l) lab, 'v) rseq) list"
    8.42 +type_synonym ('f, 'l, 'v) dppLL   =
    8.43 +  "bool \<times> bool \<times> ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL \<times>
    8.44 +  ('f, 'l, 'v) termsLL \<times>
    8.45 +  ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL"
    8.46 +
    8.47 +type_synonym ('f, 'l, 'v) qreltrsLL =
    8.48 +  "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL"
    8.49 +
    8.50 +type_synonym ('f, 'l, 'v) qtrsLL =
    8.51 +  "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL"
    8.52 +
    8.53 +datatype_new location = H | A | B | R
    8.54 +
    8.55 +type_synonym ('f,'v)forb_pattern = "('f,'v)ctxt \<times> ('f,'v)term \<times> location"
    8.56 +type_synonym ('f,'v)forb_patterns = "('f,'v)forb_pattern set"
    8.57 +
    8.58 +type_synonym ('f, 'l, 'v) fptrsLL =
    8.59 +  "(('f, 'l)lab, 'v) forb_pattern list \<times> ('f, 'l, 'v) trsLL"
    8.60 +
    8.61 +type_synonym ('f, 'l, 'v) prob = "('f, 'l, 'v) qreltrsLL + ('f, 'l, 'v) dppLL"
    8.62 +
    8.63 +type_synonym ('f, 'a) lpoly_inter = "'f \<times> nat \<Rightarrow> ('a \<times> 'a list)"
    8.64 +type_synonym ('f, 'a) lpoly_interL = "(('f \<times> nat) \<times> ('a \<times> 'a list)) list"
    8.65 +
    8.66 +type_synonym 'v monom = "('v \<times> nat)list" 
    8.67 +type_synonym ('v,'a)poly = "('v monom \<times> 'a)list"
    8.68 +type_synonym ('f,'a)poly_inter_list = "(('f \<times> nat) \<times> (nat,'a)poly)list"
    8.69 +type_synonym 'a vec = "'a list"
    8.70 +type_synonym 'a mat = "'a vec list" 
    8.71 +
    8.72 +
    8.73 +datatype_new arctic = MinInfty | Num_arc int
    8.74 +datatype_new 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a
    8.75 +datatype_new order_tag = Lex | Mul
    8.76 +
    8.77 +type_synonym 'f status_prec_repr = "(('f \<times> nat) \<times> (nat \<times> order_tag))list"
    8.78 +datatype_new af_entry = Collapse nat | AFList "nat list"
    8.79 +type_synonym 'f afs_list = "(('f \<times> nat) \<times> af_entry)list"
    8.80 +type_synonym 'f prec_weight_repr = "(('f \<times> nat) \<times> (nat \<times> nat \<times> (nat list option)))list \<times> nat"
    8.81 +
    8.82 +
    8.83 +datatype_new 'f redtriple_impl = 
    8.84 +    Int_carrier "('f, int) lpoly_interL" 
    8.85 +  | Int_nl_carrier "('f, int) poly_inter_list" 
    8.86 +  | Rat_carrier "('f, rat) lpoly_interL"
    8.87 +  | Rat_nl_carrier rat "('f, rat) poly_inter_list"
    8.88 +  | Real_carrier "('f, real) lpoly_interL"
    8.89 +  | Real_nl_carrier real "('f, real) poly_inter_list"
    8.90 +  | Arctic_carrier "('f, arctic) lpoly_interL" 
    8.91 +  | Arctic_rat_carrier "('f, rat arctic_delta) lpoly_interL" 
    8.92 +  | Int_mat_carrier nat nat "('f, int mat) lpoly_interL"
    8.93 +  | Rat_mat_carrier nat nat "('f, rat mat) lpoly_interL"
    8.94 +  | Real_mat_carrier nat nat "('f, real mat) lpoly_interL"
    8.95 +  | Arctic_mat_carrier nat "('f, arctic mat) lpoly_interL"
    8.96 +  | Arctic_rat_mat_carrier nat "('f, rat arctic_delta mat) lpoly_interL"
    8.97 +  | RPO "'f status_prec_repr" "'f afs_list"
    8.98 +  | KBO "'f prec_weight_repr" "'f afs_list"
    8.99 +
   8.100 +datatype_new list_order_type = MS_Ext | Max_Ext | Min_Ext  | Dms_Ext 
   8.101 +type_synonym 'f scnp_af = "(('f \<times> nat) \<times> (nat \<times> nat) list) list"
   8.102 +
   8.103 +datatype_new 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl"
   8.104 +
   8.105 +type_synonym 'f sig_map_list = "(('f \<times> nat) \<times> 'f list) list"
   8.106 +type_synonym ('f,'v) uncurry_info = "'f \<times> 'f sig_map_list \<times> ('f,'v)rules \<times> ('f,'v)rules"
   8.107 +
   8.108 +datatype_new arithFun =
   8.109 +  Arg nat
   8.110 +| Const nat
   8.111 +| Sum "arithFun list"
   8.112 +| Max "arithFun list"
   8.113 +| Min "arithFun list"
   8.114 +| Prod "arithFun list"
   8.115 +| IfEqual arithFun arithFun arithFun arithFun
   8.116 +
   8.117 +datatype_new 'f sl_inter = SL_Inter nat "(('f \<times> nat) \<times> arithFun) list"
   8.118 +datatype_new ('f,'v)sl_variant = Rootlab "('f \<times> nat) option" | Finitelab "'f sl_inter" | QuasiFinitelab "'f sl_inter" 'v
   8.119 +
   8.120 +type_synonym ('f,'v)crit_pair_joins = "(('f,'v)term \<times> ('f,'v)rseq \<times> ('f,'v)term \<times> ('f,'v)rseq)list"
   8.121 +datatype_new 'f join_info = Guided "('f,string)crit_pair_joins" | Join_NF | Join_BFS nat
   8.122 +
   8.123 +type_synonym unknown_info = string
   8.124 +
   8.125 +type_synonym dummy_prf = unit
   8.126 +
   8.127 +
   8.128 +datatype_new ('f,'v)complex_constant_removal_prf = Complex_Constant_Removal_Proof 
   8.129 +  "('f,'v)term" 
   8.130 +  "(('f,'v)rule \<times> ('f,'v)rule) list" 
   8.131 +
   8.132 +datatype_new ('f,'v)cond_constraint 
   8.133 +  = CC_cond bool "('f,'v)rule" 
   8.134 +  | CC_rewr "('f,'v)term" "('f,'v)term"
   8.135 +  | CC_impl "('f,'v)cond_constraint list" "('f,'v)cond_constraint"
   8.136 +  | CC_all 'v "('f,'v)cond_constraint"
   8.137 +
   8.138 +type_synonym ('f, 'v, 'w) gsubstL = "('v \<times> ('f, 'w) term) list"
   8.139 +type_synonym ('f, 'v) substL = "('f, 'v, 'v) gsubstL"
   8.140 +
   8.141 +datatype_new ('f,'v)cond_constraint_prf = 
   8.142 +  Final 
   8.143 +| Delete_Condition "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf"
   8.144 +| Different_Constructor "('f,'v)cond_constraint"
   8.145 +| Same_Constructor "('f,'v)cond_constraint" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf"
   8.146 +| Variable_Equation 'v "('f,'v)term" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf"
   8.147 +| Funarg_Into_Var "('f,'v)cond_constraint" nat 'v "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf"
   8.148 +| Simplify_Condition "('f,'v)cond_constraint" "('f,'v)substL" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf"
   8.149 +| Induction "('f,'v)cond_constraint" "('f,'v)cond_constraint list" "(('f,'v)rule \<times> (('f,'v)term \<times> 'v list) list \<times> ('f,'v)cond_constraint \<times> ('f,'v)cond_constraint_prf) list"
   8.150 +
   8.151 +
   8.152 +datatype_new ('f,'v)cond_red_pair_prf = Cond_Red_Pair_Prf 
   8.153 +  'f 
   8.154 +  "(('f,'v)cond_constraint \<times> ('f,'v)rules \<times> ('f,'v)cond_constraint_prf) list"
   8.155 +  nat 
   8.156 +  nat 
   8.157 +
   8.158 +datatype_new ('q,'f)ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _")
   8.159 +datatype_new ('q,'f)tree_automaton = Tree_Automaton "'q list" "('q,'f)ta_rule list" "('q \<times> 'q)list"
   8.160 +datatype_new 'q ta_relation = Decision_Proc | Id_Relation | Some_Relation "('q \<times> 'q) list"
   8.161 +
   8.162 +datatype_new boundstype = Roof | Match
   8.163 +datatype_new ('f,'q)bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation"
   8.164 +
   8.165 +datatype_new ('f, 'v) pat_eqv_prf =
   8.166 +  Pat_Dom_Renaming "('f, 'v) substL"
   8.167 +| Pat_Irrelevant "('f, 'v) substL" "('f, 'v) substL"
   8.168 +| Pat_Simplify "('f, 'v) substL" "('f, 'v) substL"
   8.169 +
   8.170 +datatype_new pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close
   8.171 +
   8.172 +datatype_new ('f, 'v) pat_rule_prf = 
   8.173 +  Pat_OrigRule "('f, 'v) rule" bool
   8.174 +| Pat_InitPump "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL"
   8.175 +| Pat_InitPumpCtxt "('f, 'v) pat_rule_prf" "('f, 'v) substL" pos 'v
   8.176 +| Pat_Equiv "('f, 'v) pat_rule_prf" bool "('f, 'v) pat_eqv_prf"
   8.177 +| Pat_Narrow "('f, 'v) pat_rule_prf" "('f, 'v) pat_rule_prf" pos
   8.178 +| Pat_Inst "('f, 'v) pat_rule_prf" "('f, 'v) substL" pat_rule_pos
   8.179 +| Pat_Rewr "('f, 'v) pat_rule_prf" "('f, 'v) term \<times> ('f, 'v) rseq" pat_rule_pos 'v 
   8.180 +| Pat_Exp_Sigma "('f, 'v) pat_rule_prf" nat
   8.181 +
   8.182 +datatype_new ('f, 'v) non_loop_prf =
   8.183 +  Non_Loop_Prf "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" nat nat pos
   8.184 +
   8.185 +
   8.186 +datatype_new ('f, 'l, 'v) problem = 
   8.187 +  SN_TRS "('f,'l,'v)qreltrsLL"
   8.188 +| SN_FP_TRS "('f,'l,'v)fptrsLL" 
   8.189 +| Finite_DPP "('f,'l,'v) dppLL"
   8.190 +| Unknown_Problem unknown_info
   8.191 +| Not_SN_TRS "('f,'l,'v)qtrsLL" 
   8.192 +| Not_RelSN_TRS "('f,'l,'v)qreltrsLL" 
   8.193 +| Infinite_DPP "('f,'l,'v) dppLL"
   8.194 +| Not_SN_FP_TRS "('f,'l,'v)fptrsLL" 
   8.195 +declare [[bnf_timing]]
   8.196 +datatype_new ('f, 'l, 'v, 'a, 'b, 'c, 'd, 'e) generic_assm_proof = 
   8.197 +  SN_assm_proof "('f,'l,'v)qreltrsLL" 'a
   8.198 +| Finite_assm_proof "('f,'l,'v)dppLL" 'b
   8.199 +| SN_FP_assm_proof "('f,'l,'v)fptrsLL" 'c
   8.200 +| Not_SN_assm_proof "('f,'l,'v)qtrsLL" 'a
   8.201 +| Infinite_assm_proof "('f,'l,'v)dppLL" 'b
   8.202 +| Not_RelSN_assm_proof "('f,'l,'v)qreltrsLL" 'c
   8.203 +| Not_SN_FP_assm_proof "('f,'l,'v)fptrsLL" 'd
   8.204 +| Unknown_assm_proof unknown_info 'e
   8.205 +
   8.206 +type_synonym ('f,'l,'v,'a,'b,'c,'d)assm_proof = "('f,'l,'v,'a,'b,'c,dummy_prf,'d)generic_assm_proof"
   8.207 +
   8.208 +datatype_new ('f, 'l, 'v) assm = 
   8.209 +  SN_assm "('f,'l,'v)problem list" "('f,'l,'v)qreltrsLL" 
   8.210 +| SN_FP_assm "('f,'l,'v)problem list" "('f,'l,'v)fptrsLL"
   8.211 +| Finite_assm "('f,'l,'v)problem list" "('f,'l,'v)dppLL"
   8.212 +| Unknown_assm "('f,'l,'v)problem list" unknown_info
   8.213 +| Not_SN_assm "('f,'l,'v)problem list" "('f,'l,'v)qtrsLL" 
   8.214 +| Not_RelSN_assm "('f,'l,'v)problem list" "('f,'l,'v)qreltrsLL" 
   8.215 +| Not_SN_FP_assm "('f,'l,'v)problem list" "('f,'l,'v)fptrsLL"
   8.216 +| Infinite_assm "('f,'l,'v)problem list" "('f,'l,'v)dppLL"
   8.217 +
   8.218 +fun satisfied :: "('f,'l,'v)problem \<Rightarrow> bool" where
   8.219 +  "satisfied (SN_TRS t) = (t = t)"
   8.220 +| "satisfied (SN_FP_TRS t) = (t \<noteq> t)"
   8.221 +| "satisfied (Finite_DPP d) = (d \<noteq> d)"
   8.222 +| "satisfied (Unknown_Problem s) = (s = ''foo'')"
   8.223 +| "satisfied (Not_SN_TRS (nfs,q,r)) = (length q = length r)"
   8.224 +| "satisfied (Not_RelSN_TRS (nfs,q,r,rw)) = (r = rw)"
   8.225 +| "satisfied (Infinite_DPP d) = (d = d)"
   8.226 +| "satisfied (Not_SN_FP_TRS t) = (t = t)"
   8.227 +
   8.228 +fun collect_assms :: "('tp \<Rightarrow> ('f,'l,'v) assm list) 
   8.229 +  \<Rightarrow> ('dpp \<Rightarrow> ('f,'l,'v) assm list)
   8.230 +  \<Rightarrow> ('fptp \<Rightarrow> ('f,'l,'v) assm list)
   8.231 +  \<Rightarrow> ('unk \<Rightarrow> ('f,'l,'v) assm list)
   8.232 +  \<Rightarrow> ('f,'l,'v,'tp,'dpp,'fptp,'unk) assm_proof \<Rightarrow> ('f,'l,'v) assm list" where
   8.233 +  "collect_assms tp dpp fptp unk (SN_assm_proof t prf) = tp prf"
   8.234 +| "collect_assms tp dpp fptp unk (SN_FP_assm_proof t prf) = fptp prf"
   8.235 +| "collect_assms tp dpp fptp unk (Finite_assm_proof d prf) = dpp prf"
   8.236 +| "collect_assms tp dpp fptp unk (Unknown_assm_proof p prf) = unk prf"
   8.237 +| "collect_assms _ _ _ _ _ = []"
   8.238 +
   8.239 +fun collect_neg_assms :: "('tp \<Rightarrow> ('f,'l,'v) assm list) 
   8.240 +  \<Rightarrow> ('dpp \<Rightarrow> ('f,'l,'v) assm list)
   8.241 +  \<Rightarrow> ('rtp \<Rightarrow> ('f,'l,'v) assm list)
   8.242 +  \<Rightarrow> ('fptp \<Rightarrow> ('f,'l,'v) assm list)
   8.243 +  \<Rightarrow> ('unk \<Rightarrow> ('f,'l,'v) assm list) 
   8.244 +  \<Rightarrow> ('f,'l,'v,'tp,'dpp,'rtp,'fptp,'unk) generic_assm_proof \<Rightarrow> ('f,'l,'v) assm list" where
   8.245 +  "collect_neg_assms tp dpp rtp fptp unk (Not_SN_assm_proof t prf) = tp prf"
   8.246 +| "collect_neg_assms tp dpp rtp fptp unk (Infinite_assm_proof d prf) = dpp prf"
   8.247 +| "collect_neg_assms tp dpp rtp fptp unk (Not_RelSN_assm_proof t prf) = rtp prf"
   8.248 +| "collect_neg_assms tp dpp rtp fptp unk (Not_SN_FP_assm_proof t prf) = fptp prf"
   8.249 +| "collect_neg_assms tp dpp rtp fptp unk (Unknown_assm_proof p prf) = unk prf"
   8.250 +| "collect_neg_assms tp dpp rtp fptp unk _ = []"
   8.251 +
   8.252 +
   8.253 +
   8.254 +datatype_new ('f, 'l, 'v) dp_nontermination_proof =
   8.255 +  DP_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) prseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt"
   8.256 +| DP_Nonloop "(('f,'l)lab, 'v)non_loop_prf"
   8.257 +| DP_Rule_Removal "('f,'l,'v)trsLL option" "('f,'l,'v)trsLL option" "('f,'l,'v) dp_nontermination_proof"
   8.258 +| DP_Q_Increase "('f,'l,'v)termsLL" "('f,'l,'v) dp_nontermination_proof"
   8.259 +| DP_Q_Reduction "('f,'l,'v)termsLL" "('f,'l,'v) dp_nontermination_proof"
   8.260 +| DP_Termination_Switch "('f,'l)lab join_info" "('f,'l,'v) dp_nontermination_proof"
   8.261 +| DP_Instantiation "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof"
   8.262 +| DP_Rewriting "('f,'l,'v)trsLL option" "('f,'l,'v)ruleLL" "('f,'l,'v)ruleLL" "('f,'l,'v)ruleLL" "(('f,'l)lab,'v)rule" pos "('f,'l,'v) dp_nontermination_proof"
   8.263 +| DP_Narrowing "('f,'l,'v)ruleLL" pos "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof"
   8.264 +| DP_Assume_Infinite  "('f, 'l, 'v) dppLL" 
   8.265 +    "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof,
   8.266 +     ('f, 'l, 'v) dp_nontermination_proof, 
   8.267 +     ('f, 'l, 'v) reltrs_nontermination_proof, 
   8.268 +     ('f, 'l, 'v) fp_nontermination_proof,
   8.269 +     ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   8.270 + and
   8.271 +('f,'l,'v) "trs_nontermination_proof" = 
   8.272 +  TRS_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) rseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt"
   8.273 +| TRS_Not_Well_Formed
   8.274 +| TRS_Rule_Removal "('f,'l,'v)trsLL" "('f,'l,'v) trs_nontermination_proof"
   8.275 +| TRS_String_Reversal "('f,'l,'v) trs_nontermination_proof"
   8.276 +| TRS_DP_Trans "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof"
   8.277 +| TRS_Nonloop "(('f,'l)lab,'v) non_loop_prf"
   8.278 +| TRS_Q_Increase "('f,'l,'v)termsLL" "('f,'l,'v) trs_nontermination_proof"
   8.279 +| TRS_Assume_Not_SN  "('f, 'l, 'v)qtrsLL" 
   8.280 +    "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof,
   8.281 +     ('f, 'l, 'v) dp_nontermination_proof, 
   8.282 +     ('f, 'l, 'v) reltrs_nontermination_proof, 
   8.283 +     ('f, 'l, 'v) fp_nontermination_proof,
   8.284 +     ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   8.285 + and
   8.286 +('f,'l,'v)"reltrs_nontermination_proof" = 
   8.287 +  Rel_Loop "(('f,'l)lab,'v) term" "(('f,'l)lab, 'v) prseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt"
   8.288 +| Rel_Not_Well_Formed
   8.289 +| Rel_Rule_Removal "('f,'l,'v)trsLL option" "('f,'l,'v)trsLL option" "('f,'l,'v) reltrs_nontermination_proof"
   8.290 +| Rel_R_Not_SN "('f,'l,'v) trs_nontermination_proof"
   8.291 +| Rel_TRS_Assume_Not_SN  "('f, 'l, 'v)qreltrsLL" 
   8.292 +    "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof,
   8.293 +     ('f, 'l, 'v) dp_nontermination_proof, 
   8.294 +     ('f, 'l, 'v) reltrs_nontermination_proof, 
   8.295 +     ('f, 'l, 'v) fp_nontermination_proof,
   8.296 +     ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   8.297 + and
   8.298 + ('f, 'l, 'v) "fp_nontermination_proof" = 
   8.299 +  FPTRS_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) rseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt"
   8.300 +| FPTRS_Rule_Removal "('f,'l,'v)trsLL" "('f,'l,'v) fp_nontermination_proof" 
   8.301 +| FPTRS_Assume_Not_SN  "('f, 'l, 'v)fptrsLL" 
   8.302 +    "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof,
   8.303 +     ('f, 'l, 'v) dp_nontermination_proof, 
   8.304 +     ('f, 'l, 'v) reltrs_nontermination_proof, 
   8.305 +     ('f, 'l, 'v) fp_nontermination_proof,
   8.306 +     ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   8.307 + and
   8.308 + ('f, 'l, 'v) neg_unknown_proof =
   8.309 +  Assume_NT_Unknown unknown_info 
   8.310 +    "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof,
   8.311 +     ('f, 'l, 'v) dp_nontermination_proof, 
   8.312 +     ('f, 'l, 'v) reltrs_nontermination_proof, 
   8.313 +     ('f, 'l, 'v) fp_nontermination_proof,
   8.314 +     ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list"
   8.315 +
   8.316 +
   8.317 +datatype_new ('f, 'l, 'v) dp_termination_proof =
   8.318 +  P_is_Empty
   8.319 +| Subterm_Criterion_Proc "('f, 'l) lab projL" "('f, 'l, 'v) rseqL"
   8.320 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   8.321 +| Redpair_Proc "('f,'l)lab root_redtriple_impl + ('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL"  "('f, 'l, 'v) dp_termination_proof"
   8.322 +| Redpair_UR_Proc "('f, 'l) lab root_redtriple_impl + ('f, 'l) lab redtriple_impl"
   8.323 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" 
   8.324 +| Usable_Rules_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" 
   8.325 +| Dep_Graph_Proc "(('f, 'l, 'v) dp_termination_proof option \<times> ('f, 'l, 'v) trsLL) list"
   8.326 +| Mono_Redpair_Proc "('f, 'l) lab redtriple_impl"
   8.327 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" 
   8.328 +| Mono_Redpair_UR_Proc "('f, 'l) lab redtriple_impl"
   8.329 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   8.330 +| Size_Change_Subterm_Proc "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list"
   8.331 +| Size_Change_Redpair_Proc "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL option"
   8.332 +    "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list"
   8.333 +| Uncurry_Proc "nat option" "(('f, 'l) lab, 'v) uncurry_info"
   8.334 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   8.335 +| Fcc_Proc "('f, 'l) lab" "(('f, 'l) lab, 'v) ctxt list"
   8.336 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   8.337 +| Split_Proc
   8.338 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" 
   8.339 +    "('f, 'l, 'v) dp_termination_proof" "('f, 'l, 'v) dp_termination_proof"
   8.340 +| Semlab_Proc
   8.341 +    "(('f, 'l) lab, 'v) sl_variant" "('f, 'l, 'v) trsLL"
   8.342 +    "(('f, 'l) lab, 'v) term list" "('f, 'l, 'v) trsLL"
   8.343 +    "('f, 'l, 'v) dp_termination_proof"
   8.344 +| Switch_Innermost_Proc "('f, 'l) lab join_info" "('f, 'l, 'v) dp_termination_proof"
   8.345 +| Rewriting_Proc
   8.346 +    "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL"
   8.347 +    "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) dp_termination_proof"
   8.348 +| Instantiation_Proc "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   8.349 +| Forward_Instantiation_Proc
   8.350 +    "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_termination_proof"
   8.351 +| Narrowing_Proc "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   8.352 +| Assume_Finite
   8.353 +    "('f, 'l, 'v) dppLL" "('f,'l,'v,('f, 'l, 'v) trs_termination_proof,('f, 'l, 'v) dp_termination_proof,('f, 'l, 'v) fptrs_termination_proof,('f, 'l, 'v) unknown_proof) assm_proof list"
   8.354 +| Unlab_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof"
   8.355 +| Q_Reduction_Proc "('f, 'l, 'v) termsLL" "('f, 'l, 'v) dp_termination_proof"
   8.356 +| Complex_Constant_Removal_Proc "(('f,'l)lab,'v)complex_constant_removal_prf" "('f, 'l, 'v) dp_termination_proof"
   8.357 +| General_Redpair_Proc
   8.358 +    "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL"
   8.359 +    "(('f, 'l) lab, 'v) cond_red_pair_prf" "('f, 'l, 'v) dp_termination_proof list" 
   8.360 +| To_Trs_Proc "('f, 'l, 'v) trs_termination_proof"
   8.361 +and ('f, 'l, 'v) trs_termination_proof =
   8.362 +  DP_Trans bool bool "(('f, 'l) lab, 'v) rules" "('f, 'l, 'v) dp_termination_proof"
   8.363 +| Rule_Removal "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v)trs_termination_proof"
   8.364 +| String_Reversal "('f, 'l, 'v) trs_termination_proof"
   8.365 +| Bounds "(('f, 'l) lab, 'v) bounds_info"
   8.366 +| Uncurry "(('f, 'l) lab, 'v) uncurry_info" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   8.367 +| Semlab
   8.368 +    "(('f, 'l) lab, 'v) sl_variant" "(('f, 'l) lab, 'v) term list"
   8.369 +    "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   8.370 +| R_is_Empty
   8.371 +| Fcc "(('f, 'l) lab, 'v) ctxt list" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   8.372 +| Split "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" "('f, 'l, 'v) trs_termination_proof"
   8.373 +| Switch_Innermost "('f, 'l) lab join_info" "('f, 'l, 'v) trs_termination_proof" 
   8.374 +| Drop_Equality "('f, 'l, 'v) trs_termination_proof"
   8.375 +| Remove_Nonapplicable_Rules "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof"
   8.376 +| Assume_SN "('f, 'l, 'v) qreltrsLL" "('f,'l,'v,('f, 'l, 'v) trs_termination_proof,('f, 'l, 'v) dp_termination_proof,('f, 'l, 'v) fptrs_termination_proof,('f, 'l, 'v) unknown_proof) assm_proof list"
   8.377 +and ('f, 'l, 'v) unknown_proof =
   8.378 +  Assume_Unknown unknown_info "('f,'l,'v,('f, 'l, 'v) trs_termination_proof,('f, 'l, 'v) dp_termination_proof,('f, 'l, 'v) fptrs_termination_proof,('f, 'l, 'v) unknown_proof) assm_proof list"
   8.379 +and ('f, 'l, 'v) fptrs_termination_proof =
   8.380 +  Assume_FP_SN "('f,'l,'v)fptrsLL" "('f,'l,'v,('f, 'l, 'v) trs_termination_proof,('f, 'l, 'v) dp_termination_proof,('f, 'l, 'v) fptrs_termination_proof,('f, 'l, 'v) unknown_proof) assm_proof list"
   8.381 +
   8.382 +
   8.383 +end
     9.1 --- a/src/HOL/ROOT	Mon Jul 21 17:57:16 2014 +0200
     9.2 +++ b/src/HOL/ROOT	Tue Jul 22 08:07:47 2014 +0200
     9.3 @@ -734,6 +734,8 @@
     9.4      Misc_Datatype
     9.5      Misc_Primcorec
     9.6      Misc_Primrec
     9.7 +  theories [condition = ISABELLE_FULL_TEST]
     9.8 +    IsaFoR_Datatypes
     9.9  
    9.10  session "HOL-Word" (main) in Word = HOL +
    9.11    options [document_graph]
    10.1 --- a/src/Pure/General/completion.scala	Mon Jul 21 17:57:16 2014 +0200
    10.2 +++ b/src/Pure/General/completion.scala	Tue Jul 22 08:07:47 2014 +0200
    10.3 @@ -11,6 +11,7 @@
    10.4  
    10.5  import scala.collection.immutable.SortedMap
    10.6  import scala.util.parsing.combinator.RegexParsers
    10.7 +import scala.util.matching.Regex
    10.8  import scala.math.Ordering
    10.9  
   10.10  
   10.11 @@ -219,6 +220,9 @@
   10.12    {
   10.13      override val whiteSpace = "".r
   10.14  
   10.15 +    private val symbol_regex: Regex = """\\<\^?[A-Za-z0-9_']+>""".r
   10.16 +    def is_symbol(s: CharSequence): Boolean = symbol_regex.pattern.matcher(s).matches
   10.17 +
   10.18      private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
   10.19      private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
   10.20      private def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
   10.21 @@ -231,16 +235,6 @@
   10.22      def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
   10.23      def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.'
   10.24  
   10.25 -    def extend_word(text: CharSequence, offset: Text.Offset): Text.Offset =
   10.26 -    {
   10.27 -      val n = text.length
   10.28 -      var i = offset
   10.29 -      while (i < n && is_word_char(text.charAt(i))) i += 1
   10.30 -      if (i < n && text.charAt(i) == '>' && read_symbol(text.subSequence(0, i + 1)).isDefined)
   10.31 -        i + 1
   10.32 -      else i
   10.33 -    }
   10.34 -
   10.35      def read_symbol(in: CharSequence): Option[String] =
   10.36      {
   10.37        val reverse_in = new Library.Reverse(in)
   10.38 @@ -341,7 +335,6 @@
   10.39      start: Text.Offset,
   10.40      text: CharSequence,
   10.41      caret: Int,
   10.42 -    extend_word: Boolean,
   10.43      language_context: Completion.Language_Context): Option[Completion.Result] =
   10.44    {
   10.45      def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
   10.46 @@ -358,8 +351,11 @@
   10.47              case (a, _) :: _ =>
   10.48                val ok =
   10.49                  if (a == Completion.antiquote) language_context.antiquotes
   10.50 -                else language_context.symbols || Completion.default_abbrs.exists(_._1 == a)
   10.51 -              if (ok) Some(((a, abbrevs), caret))
   10.52 +                else
   10.53 +                  language_context.symbols ||
   10.54 +                  Completion.default_abbrs.exists(_._1 == a) ||
   10.55 +                  Completion.Word_Parsers.is_symbol(a)
   10.56 +              if (ok) Some((a, abbrevs))
   10.57                else None
   10.58            }
   10.59          case _ => None
   10.60 @@ -369,17 +365,10 @@
   10.61      val words_result =
   10.62        if (abbrevs_result.isDefined) None
   10.63        else {
   10.64 -        val end =
   10.65 -          if (extend_word) Completion.Word_Parsers.extend_word(text, caret)
   10.66 -          else caret
   10.67          val result =
   10.68 -          Completion.Word_Parsers.read_symbol(text.subSequence(0, end)) match {
   10.69 +          Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match {
   10.70              case Some(symbol) => Some((symbol, ""))
   10.71 -            case None =>
   10.72 -              val word_context =
   10.73 -                end < length && Completion.Word_Parsers.is_word_char(text.charAt(end))
   10.74 -              if (word_context) None
   10.75 -              else Completion.Word_Parsers.read_word(explicit, text.subSequence(0, end))
   10.76 +            case None => Completion.Word_Parsers.read_word(explicit, text.subSequence(0, caret))
   10.77            }
   10.78          result.map(
   10.79            {
   10.80 @@ -397,13 +386,13 @@
   10.81                      if ok
   10.82                      completion <- words_map.get_list(complete_word)
   10.83                    } yield (complete_word, completion)
   10.84 -              (((full_word, completions), end))
   10.85 +              ((full_word, completions))
   10.86            })
   10.87        }
   10.88  
   10.89      (abbrevs_result orElse words_result) match {
   10.90 -      case Some(((original, completions), end)) if !completions.isEmpty =>
   10.91 -        val range = Text.Range(- original.length, 0) + end + start
   10.92 +      case Some((original, completions)) if !completions.isEmpty =>
   10.93 +        val range = Text.Range(- original.length, 0) + caret + start
   10.94          val immediate =
   10.95            explicit ||
   10.96              (!Completion.Word_Parsers.is_word(original) &&
    11.1 --- a/src/Pure/PIDE/markup.ML	Mon Jul 21 17:57:16 2014 +0200
    11.2 +++ b/src/Pure/PIDE/markup.ML	Tue Jul 22 08:07:47 2014 +0200
    11.3 @@ -185,6 +185,7 @@
    11.4    val use_theories_result: string -> bool -> Properties.T
    11.5    val print_operationsN: string
    11.6    val print_operations: Properties.T
    11.7 +  val simp_trace_panelN: string
    11.8    val simp_trace_logN: string
    11.9    val simp_trace_stepN: string
   11.10    val simp_trace_recurseN: string
   11.11 @@ -586,6 +587,8 @@
   11.12  
   11.13  (* simplifier trace *)
   11.14  
   11.15 +val simp_trace_panelN = "simp_trace_panel";
   11.16 +
   11.17  val simp_trace_logN = "simp_trace_log";
   11.18  val simp_trace_stepN = "simp_trace_step";
   11.19  val simp_trace_recurseN = "simp_trace_recurse";
    12.1 --- a/src/Pure/PIDE/markup.scala	Mon Jul 21 17:57:16 2014 +0200
    12.2 +++ b/src/Pure/PIDE/markup.scala	Tue Jul 22 08:07:47 2014 +0200
    12.3 @@ -464,7 +464,7 @@
    12.4  
    12.5    /* simplifier trace */
    12.6  
    12.7 -  val SIMP_TRACE = "simp_trace"
    12.8 +  val SIMP_TRACE_PANEL = "simp_trace_panel"
    12.9  
   12.10    val SIMP_TRACE_LOG = "simp_trace_log"
   12.11    val SIMP_TRACE_STEP = "simp_trace_step"
    13.1 --- a/src/Pure/Tools/simplifier_trace.ML	Mon Jul 21 17:57:16 2014 +0200
    13.2 +++ b/src/Pure/Tools/simplifier_trace.ML	Tue Jul 22 08:07:47 2014 +0200
    13.3 @@ -60,36 +60,43 @@
    13.4       breakpoints = merge_breakpoints (breakpoints1, breakpoints2)}: T
    13.5  )
    13.6  
    13.7 -fun map_breakpoints f_term f_thm =
    13.8 +val get_data = Data.get o Context.Proof
    13.9 +val put_data = Context.proof_map o Data.put
   13.10 +
   13.11 +val get_breakpoints = #breakpoints o get_data
   13.12 +
   13.13 +fun map_breakpoints f =
   13.14    Data.map
   13.15 -    (fn {max_depth, mode, interactive, parent, memory, breakpoints = (term_bs, thm_bs)} =>
   13.16 +    (fn {max_depth, mode, interactive, parent, memory, breakpoints} =>
   13.17        {max_depth = max_depth,
   13.18         mode = mode,
   13.19         interactive = interactive,
   13.20         memory = memory,
   13.21         parent = parent,
   13.22 -       breakpoints = (f_term term_bs, f_thm thm_bs)})
   13.23 +       breakpoints = f breakpoints})
   13.24  
   13.25  fun add_term_breakpoint term =
   13.26 -  map_breakpoints (Item_Net.update term) I
   13.27 +  map_breakpoints (apfst (Item_Net.update term))
   13.28  
   13.29  fun add_thm_breakpoint thm context =
   13.30    let
   13.31      val rrules = mk_rrules (Context.proof_of context) [thm]
   13.32    in
   13.33 -    map_breakpoints I (fold Item_Net.update rrules) context
   13.34 +    map_breakpoints (apsnd (fold Item_Net.update rrules)) context
   13.35    end
   13.36  
   13.37 -fun is_breakpoint (term, rrule) context =
   13.38 +fun check_breakpoint (term, rrule) ctxt =
   13.39    let
   13.40 -    val {breakpoints, ...} = Data.get context
   13.41 +    val thy = Proof_Context.theory_of ctxt
   13.42 +    val (term_bs, thm_bs) = get_breakpoints ctxt
   13.43  
   13.44 -    fun matches pattern = Pattern.matches (Context.theory_of context) (pattern, term)
   13.45 -    val term_matches = filter matches (Item_Net.retrieve_matching (fst breakpoints) term)
   13.46 +    val term_matches =
   13.47 +      filter (fn pat => Pattern.matches thy (pat, term))
   13.48 +        (Item_Net.retrieve_matching term_bs term)
   13.49  
   13.50 -    val {thm = thm, ...} = rrule
   13.51 -    val thm_matches = exists (eq_rrule o pair rrule)
   13.52 -      (Item_Net.retrieve_matching (snd breakpoints) (Thm.full_prop_of thm))
   13.53 +    val thm_matches =
   13.54 +      exists (eq_rrule o pair rrule)
   13.55 +        (Item_Net.retrieve_matching thm_bs (Thm.full_prop_of (#thm rrule)))
   13.56    in
   13.57      (term_matches, thm_matches)
   13.58    end
   13.59 @@ -146,7 +153,7 @@
   13.60  
   13.61  fun mk_generic_result markup text triggered (payload : unit -> payload) ctxt =
   13.62    let
   13.63 -    val {mode, interactive, memory, parent, ...} = Data.get (Context.Proof ctxt)
   13.64 +    val {mode, interactive, memory, parent, ...} = get_data ctxt
   13.65  
   13.66      val eligible =
   13.67        (case mode of
   13.68 @@ -178,6 +185,14 @@
   13.69  
   13.70  (** tracing output **)
   13.71  
   13.72 +fun see_panel () =
   13.73 +  let
   13.74 +    val ((bg1, bg2), en) =
   13.75 +      YXML.output_markup_elem
   13.76 +        (Active.make_markup Markup.simp_trace_panelN {implicit = false, properties = []})
   13.77 +  in "See " ^ bg1 ^ bg2 ^ "simplifier trace" ^ en end
   13.78 +
   13.79 +
   13.80  fun send_request (result_id, content) =
   13.81    let
   13.82      fun break () =
   13.83 @@ -195,7 +210,7 @@
   13.84  
   13.85  fun step ({term, thm, unconditional, ctxt, rrule}: data) =
   13.86    let
   13.87 -    val (matching_terms, thm_triggered) = is_breakpoint (term, rrule) (Context.Proof ctxt)
   13.88 +    val (matching_terms, thm_triggered) = check_breakpoint (term, rrule) ctxt
   13.89  
   13.90      val {name, ...} = rrule
   13.91      val term_triggered = not (null matching_terms)
   13.92 @@ -232,21 +247,19 @@
   13.93          {props = [], pretty = pretty}
   13.94        end
   13.95  
   13.96 -    val {max_depth, mode, interactive, memory, breakpoints, ...} =
   13.97 -      Data.get (Context.Proof ctxt)
   13.98 +    val {max_depth, mode, interactive, memory, breakpoints, ...} = get_data ctxt
   13.99  
  13.100      fun mk_promise result =
  13.101        let
  13.102          val result_id = #1 result
  13.103  
  13.104 -        fun put mode' interactive' = Data.put
  13.105 +        fun put mode' interactive' = put_data
  13.106            {max_depth = max_depth,
  13.107             mode = mode',
  13.108             interactive = interactive',
  13.109             memory = memory,
  13.110             parent = result_id,
  13.111 -           breakpoints = breakpoints} (Context.Proof ctxt) |>
  13.112 -          Context.the_proof
  13.113 +           breakpoints = breakpoints} ctxt
  13.114  
  13.115          fun to_response "skip" = NONE
  13.116            | to_response "continue" = SOME (put mode true)
  13.117 @@ -273,22 +286,23 @@
  13.118        {props = [],
  13.119         pretty = Syntax.pretty_term ctxt term}
  13.120  
  13.121 -    val {max_depth, mode, interactive, memory, breakpoints, ...} =
  13.122 -      Data.get (Context.Proof ctxt)
  13.123 +    val {max_depth, mode, interactive, memory, breakpoints, ...} = get_data ctxt
  13.124  
  13.125 -    fun put result_id = Data.put
  13.126 +    fun put result_id = put_data
  13.127        {max_depth = max_depth,
  13.128         mode = if depth >= max_depth then Disabled else mode,
  13.129         interactive = interactive,
  13.130         memory = memory,
  13.131         parent = result_id,
  13.132 -       breakpoints = breakpoints} (Context.Proof ctxt)
  13.133 -
  13.134 -    val context' =
  13.135 -      (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of
  13.136 -        NONE => put 0
  13.137 -      | SOME res => (output_result res; put (#1 res)))
  13.138 -  in Context.the_proof context' end
  13.139 +       breakpoints = breakpoints} ctxt
  13.140 +  in
  13.141 +    (case mk_generic_result Markup.simp_trace_recurseN text true payload ctxt of
  13.142 +      NONE => put 0
  13.143 +    | SOME res =>
  13.144 +       (if depth = 1 then writeln (see_panel ()) else ();
  13.145 +        output_result res;
  13.146 +        put (#1 res)))
  13.147 +  end
  13.148  
  13.149  fun indicate_failure ({term, ctxt, thm, rrule, ...}: data) ctxt' =
  13.150    let
  13.151 @@ -314,7 +328,7 @@
  13.152          {props = [(successN, "false")], pretty = pretty}
  13.153        end
  13.154  
  13.155 -    val {interactive, ...} = Data.get (Context.Proof ctxt)
  13.156 +    val {interactive, ...} = get_data ctxt
  13.157  
  13.158      fun mk_promise result =
  13.159        let
  13.160 @@ -419,7 +433,7 @@
  13.161    (Attrib.setup @{binding simp_break}
  13.162      (Scan.repeat Args.term_pattern >> breakpoint)
  13.163      "declaration of a simplifier breakpoint" #>
  13.164 -   Attrib.setup @{binding simplifier_trace} (Scan.lift config_parser)
  13.165 +   Attrib.setup @{binding simp_trace_new} (Scan.lift config_parser)
  13.166      "simplifier trace configuration")
  13.167  
  13.168  end
    14.1 --- a/src/Pure/Tools/simplifier_trace.scala	Mon Jul 21 17:57:16 2014 +0200
    14.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Tue Jul 22 08:07:47 2014 +0200
    14.3 @@ -65,7 +65,6 @@
    14.4        val continue_passive = Answer("continue_passive", "Continue (without asking)")
    14.5        val continue_disable = Answer("continue_disable", "Continue (without any trace)")
    14.6  
    14.7 -      val default = skip
    14.8        val all = List(continue, continue_trace, continue_passive, continue_disable, skip)
    14.9      }
   14.10  
   14.11 @@ -74,27 +73,12 @@
   14.12        val exit = Answer("exit", "Exit")
   14.13        val redo = Answer("redo", "Redo")
   14.14  
   14.15 -      val default = exit
   14.16        val all = List(redo, exit)
   14.17      }
   14.18    }
   14.19  
   14.20    val all_answers: List[Answer] = Answer.step.all ::: Answer.hint_fail.all
   14.21  
   14.22 -  object Active
   14.23 -  {
   14.24 -    def unapply(tree: XML.Tree): Option[(Long, Answer)] =
   14.25 -      tree match {
   14.26 -        case XML.Elem(Markup(Markup.SIMP_TRACE, props), _) =>
   14.27 -          (props, props) match {
   14.28 -            case (Markup.Serial(serial), Markup.Name(name)) =>
   14.29 -              all_answers.find(_.name == name).map((serial, _))
   14.30 -            case _ => None
   14.31 -          }
   14.32 -        case _ => None
   14.33 -      }
   14.34 -  }
   14.35 -
   14.36  
   14.37    /* GUI interaction */
   14.38  
   14.39 @@ -110,7 +94,7 @@
   14.40    private object Clear_Memory
   14.41    case class Reply(session: Session, serial: Long, answer: Answer)
   14.42  
   14.43 -  case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer)
   14.44 +  case class Question(data: Item.Data, answers: List[Answer])
   14.45  
   14.46    case class Context(
   14.47      last_serial: Long = 0L,
   14.48 @@ -207,7 +191,7 @@
   14.49                          case Some(answer) if data.memory =>
   14.50                            do_reply(session, serial, answer)
   14.51                          case _ =>
   14.52 -                          new_context += Question(data, Answer.step.all, Answer.step.default)
   14.53 +                          new_context += Question(data, Answer.step.all)
   14.54                        }
   14.55  
   14.56                      case Markup.SIMP_TRACE_HINT =>
   14.57 @@ -215,11 +199,10 @@
   14.58                          case Success(false) =>
   14.59                            results.get(data.parent) match {
   14.60                              case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
   14.61 -                              new_context +=
   14.62 -                                Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
   14.63 +                              new_context += Question(data, Answer.hint_fail.all)
   14.64                              case _ =>
   14.65                                // unknown, better send a default reply
   14.66 -                              do_reply(session, data.serial, Answer.hint_fail.default)
   14.67 +                              do_reply(session, data.serial, Answer.hint_fail.exit)
   14.68                            }
   14.69                          case _ =>
   14.70                        }
   14.71 @@ -263,8 +246,7 @@
   14.72              // current results.
   14.73  
   14.74              val items =
   14.75 -              (for { (_, Item(_, data)) <- results.iterator }
   14.76 -                yield data).toList
   14.77 +              results.iterator.collect { case (_, Item(_, data)) => data }.toList
   14.78  
   14.79              slot.fulfill(Trace(items))
   14.80  
   14.81 @@ -281,7 +263,7 @@
   14.82  
   14.83            case Reply(session, serial, answer) =>
   14.84              find_question(serial) match {
   14.85 -              case Some((id, Question(data, _, _))) =>
   14.86 +              case Some((id, Question(data, _))) =>
   14.87                  if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
   14.88                  {
   14.89                    val index = Index.of_data(data)
    15.1 --- a/src/Tools/jEdit/src/active.scala	Mon Jul 21 17:57:16 2014 +0200
    15.2 +++ b/src/Tools/jEdit/src/active.scala	Tue Jul 22 08:07:47 2014 +0200
    15.3 @@ -48,6 +48,11 @@
    15.4                    Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
    15.5                  }
    15.6  
    15.7 +              case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, _), _) =>
    15.8 +                Swing_Thread.later {
    15.9 +                  view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
   15.10 +                }
   15.11 +
   15.12                case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
   15.13                  props match {
   15.14                    case Position.Id(id) =>
   15.15 @@ -60,9 +65,6 @@
   15.16                  }
   15.17                  text_area.requestFocus
   15.18  
   15.19 -              case Simplifier_Trace.Active(serial, answer) =>
   15.20 -                Simplifier_Trace.send_reply(PIDE.session, serial, answer)
   15.21 -
   15.22                case Protocol.Dialog(id, serial, result) =>
   15.23                  model.session.dialog_result(id, serial, result)
   15.24  
    16.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Mon Jul 21 17:57:16 2014 +0200
    16.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Jul 22 08:07:47 2014 +0200
    16.3 @@ -171,7 +171,7 @@
    16.4              line_text <- JEdit_Lib.try_get_text(buffer, line_range)
    16.5              result <-
    16.6                syntax.completion.complete(
    16.7 -                history, decode, explicit, line_start, line_text, caret - line_start, false, context)
    16.8 +                history, decode, explicit, line_start, line_text, caret - line_start, context)
    16.9            } yield result
   16.10  
   16.11          case None => None
   16.12 @@ -558,7 +558,7 @@
   16.13  
   16.14            val context = syntax.language_context
   16.15  
   16.16 -          syntax.completion.complete(history, true, false, 0, text, caret, false, context) match {
   16.17 +          syntax.completion.complete(history, true, false, 0, text, caret, context) match {
   16.18              case Some(result) =>
   16.19                val fm = text_field.getFontMetrics(text_field.getFont)
   16.20                val loc =
    17.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Jul 21 17:57:16 2014 +0200
    17.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Jul 22 08:07:47 2014 +0200
    17.3 @@ -149,7 +149,7 @@
    17.4  
    17.5    private val active_elements =
    17.6      Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
    17.7 -      Markup.SENDBACK, Markup.SIMP_TRACE)
    17.8 +      Markup.SENDBACK, Markup.SIMP_TRACE_PANEL)
    17.9  
   17.10    private val tooltip_message_elements =
   17.11      Markup.Elements(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)
    18.1 --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Mon Jul 21 17:57:16 2014 +0200
    18.2 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Tue Jul 22 08:07:47 2014 +0200
    18.3 @@ -29,50 +29,38 @@
    18.4    private var current_results = Command.Results.empty
    18.5    private var current_id = 0L
    18.6    private var do_update = true
    18.7 -  private var do_auto_reply = false
    18.8  
    18.9  
   18.10    private val text_area = new Pretty_Text_Area(view)
   18.11    set_content(text_area)
   18.12  
   18.13 -  private def get_content(snapshot: Document.Snapshot, question: Simplifier_Trace.Question): XML.Tree =
   18.14 +  private def update_contents()
   18.15    {
   18.16 -    val data = question.data
   18.17  
   18.18 -    def make_button(answer: Simplifier_Trace.Answer): XML.Tree =
   18.19 -      XML.Wrapped_Elem(
   18.20 -        Markup(Markup.SIMP_TRACE, Markup.Serial(data.serial) ::: Markup.Name(answer.name)),
   18.21 -        Nil,
   18.22 -        List(XML.Text(answer.string))
   18.23 -      )
   18.24 +    Swing_Thread.require {}
   18.25  
   18.26 -    def make_block(body: XML.Body): XML.Body =
   18.27 -      List(Pretty.Block(0, body))
   18.28 +    val snapshot = current_snapshot
   18.29 +    val context = Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
   18.30  
   18.31 -    val all = Pretty.separate(
   18.32 -      XML.Text(data.text) ::
   18.33 -      data.content :::
   18.34 -      make_block(Library.separate(XML.Text(", "), question.answers map make_button))
   18.35 -    )
   18.36 -
   18.37 -    XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(all)))
   18.38 -  }
   18.39 +    answers.contents.clear()
   18.40 +    context.questions.values.toList match {
   18.41 +      case q :: _ =>
   18.42 +        val data = q.data
   18.43 +        val content = Pretty.separate(XML.Text(data.text) :: data.content)
   18.44 +        text_area.update(snapshot, Command.Results.empty, content)
   18.45 +        q.answers.foreach { answer =>
   18.46 +          answers.contents += new Button(answer.string) {
   18.47 +            reactions += {
   18.48 +              case ButtonClicked(_) =>
   18.49 +                Simplifier_Trace.send_reply(PIDE.session, data.serial, answer)
   18.50 +            }
   18.51 +          }
   18.52 +        }
   18.53 +      case Nil =>
   18.54 +        text_area.update(snapshot, Command.Results.empty, Nil)
   18.55 +    }
   18.56  
   18.57 -  private def set_context(snapshot: Document.Snapshot, context: Simplifier_Trace.Context)
   18.58 -  {
   18.59 -    Swing_Thread.require {}
   18.60 -    val questions = context.questions.values
   18.61 -    if (do_auto_reply && !questions.isEmpty)
   18.62 -    {
   18.63 -      questions.foreach(q => Simplifier_Trace.send_reply(PIDE.session, q.data.serial, q.default_answer))
   18.64 -      handle_update(do_update)
   18.65 -    }
   18.66 -    else
   18.67 -    {
   18.68 -      val contents = Pretty.separate(questions.map(get_content(snapshot, _))(collection.breakOut))
   18.69 -      text_area.update(snapshot, Command.Results.empty, contents)
   18.70 -      do_paint()
   18.71 -    }
   18.72 +    do_paint()
   18.73    }
   18.74  
   18.75    private def show_trace()
   18.76 @@ -88,14 +76,6 @@
   18.77      }
   18.78    }
   18.79  
   18.80 -  private def update_contents()
   18.81 -  {
   18.82 -    set_context(
   18.83 -      current_snapshot,
   18.84 -      Simplifier_Trace.handle_results(PIDE.session, current_id, current_results)
   18.85 -    )
   18.86 -  }
   18.87 -
   18.88    private def handle_resize()
   18.89    {
   18.90      do_paint()
   18.91 @@ -195,15 +175,6 @@
   18.92        }
   18.93      },
   18.94      new Separator(Orientation.Vertical),
   18.95 -    new CheckBox("Auto reply") {
   18.96 -      selected = do_auto_reply
   18.97 -      reactions += {
   18.98 -        case ButtonClicked(_) =>
   18.99 -          do_auto_reply = this.selected
  18.100 -          handle_update(do_update)
  18.101 -      }
  18.102 -    },
  18.103 -    new Separator(Orientation.Vertical),
  18.104      new Button("Show trace") {
  18.105        reactions += {
  18.106          case ButtonClicked(_) =>
  18.107 @@ -218,5 +189,8 @@
  18.108      }
  18.109    )
  18.110  
  18.111 +  private val answers = new Wrap_Panel(Wrap_Panel.Alignment.Left)()
  18.112 +
  18.113    add(controls.peer, BorderLayout.NORTH)
  18.114 +  add(answers.peer, BorderLayout.SOUTH)
  18.115  }