| author | Andreas Lochbihler |
| Tue, 22 Jul 2014 08:07:47 +0200 | |
| changeset 57601 | 22e810680123 |
| parent 57600 | b0ad484b7d1c (current diff) |
| parent 57597 | 5c3484b90d5c (diff) |
| child 57602 | 0f708666eb7c |
--- a/Admin/components/components.sha1 Mon Jul 21 17:57:16 2014 +0200 +++ b/Admin/components/components.sha1 Tue Jul 22 08:07: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 17:57:16 2014 +0200 +++ b/Admin/components/main Tue Jul 22 08:07: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 17:57:16 2014 +0200 +++ b/Admin/java/build Tue Jul 22 08:07: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 17:57:16 2014 +0200 +++ b/NEWS Tue Jul 22 08:07: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 17:57:16 2014 +0200 +++ b/src/Doc/Isar_Ref/Generic.thy Tue Jul 22 08:07: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 17:57:16 2014 +0200 +++ b/src/Doc/Isar_Ref/document/root.tex Tue Jul 22 08:07: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 17:57:16 2014 +0200 +++ b/src/Doc/JEdit/JEdit.thy Tue Jul 22 08:07: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. *}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BNF_Examples/IsaFoR_Datatypes.thy Tue Jul 22 08:07:47 2014 +0200 @@ -0,0 +1,380 @@ +(* Title: HOL/BNF_Examples/IsaFoR_Datatypes.thy + Author: René Thiemann + Copyright 2014 + +Benchmark of datatypes defined in IsaFoR +*) + +theory IsaFoR_Datatypes +imports + Real +begin + +datatype_new ('f, 'l) lab = + Lab "('f, 'l) lab" 'l +| FunLab "('f, 'l) lab" "('f, 'l) lab list" +| UnLab 'f +| Sharp "('f, 'l) lab" + +datatype_new 'f projL = Projection "(('f \<times> nat) \<times> nat) list" + +datatype_new ('f, 'v) "term" = Var 'v | Fun 'f "('f, 'v) term list" +datatype_new ('f, 'v) ctxt = + Hole ("\<box>") +| More 'f "('f, 'v) term list" "('f, 'v) ctxt" "('f, 'v) term list" + + +type_synonym ('f, 'v) rule = "('f, 'v) term \<times> ('f, 'v) term" +type_synonym ('f, 'v) trs = "('f, 'v) rule set" + +type_synonym ('f, 'v) rules = "('f,'v) rule list" +type_synonym ('f, 'l, 'v) ruleLL = "(('f, 'l) lab, 'v) rule" +type_synonym ('f, 'l, 'v) trsLL = "(('f, 'l) lab, 'v) rules" +type_synonym ('f, 'l, 'v) termsLL = "(('f, 'l) lab, 'v) term list" +datatype_new pos = Empty ("\<epsilon>") | PCons "nat" "pos" (infixr "<#" 70) +type_synonym ('f, 'v) prseq = "(pos \<times> ('f, 'v) rule \<times> bool \<times> ('f, 'v) term) list" +type_synonym ('f, 'v) rseq = "(pos \<times> ('f, 'v) rule \<times> ('f, 'v) term) list" + +type_synonym ('f, 'l, 'v) rseqL = "((('f, 'l) lab, 'v) rule \<times> (('f, 'l) lab, 'v) rseq) list" +type_synonym ('f, 'l, 'v) dppLL = + "bool \<times> bool \<times> ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL \<times> + ('f, 'l, 'v) termsLL \<times> + ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL" + +type_synonym ('f, 'l, 'v) qreltrsLL = + "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL \<times> ('f, 'l, 'v) trsLL" + +type_synonym ('f, 'l, 'v) qtrsLL = + "bool \<times> ('f, 'l, 'v) termsLL \<times> ('f, 'l, 'v) trsLL" + +datatype_new location = H | A | B | R + +type_synonym ('f,'v)forb_pattern = "('f,'v)ctxt \<times> ('f,'v)term \<times> location" +type_synonym ('f,'v)forb_patterns = "('f,'v)forb_pattern set" + +type_synonym ('f, 'l, 'v) fptrsLL = + "(('f, 'l)lab, 'v) forb_pattern list \<times> ('f, 'l, 'v) trsLL" + +type_synonym ('f, 'l, 'v) prob = "('f, 'l, 'v) qreltrsLL + ('f, 'l, 'v) dppLL" + +type_synonym ('f, 'a) lpoly_inter = "'f \<times> nat \<Rightarrow> ('a \<times> 'a list)" +type_synonym ('f, 'a) lpoly_interL = "(('f \<times> nat) \<times> ('a \<times> 'a list)) list" + +type_synonym 'v monom = "('v \<times> nat)list" +type_synonym ('v,'a)poly = "('v monom \<times> 'a)list" +type_synonym ('f,'a)poly_inter_list = "(('f \<times> nat) \<times> (nat,'a)poly)list" +type_synonym 'a vec = "'a list" +type_synonym 'a mat = "'a vec list" + + +datatype_new arctic = MinInfty | Num_arc int +datatype_new 'a arctic_delta = MinInfty_delta | Num_arc_delta 'a +datatype_new order_tag = Lex | Mul + +type_synonym 'f status_prec_repr = "(('f \<times> nat) \<times> (nat \<times> order_tag))list" +datatype_new af_entry = Collapse nat | AFList "nat list" +type_synonym 'f afs_list = "(('f \<times> nat) \<times> af_entry)list" +type_synonym 'f prec_weight_repr = "(('f \<times> nat) \<times> (nat \<times> nat \<times> (nat list option)))list \<times> nat" + + +datatype_new 'f redtriple_impl = + Int_carrier "('f, int) lpoly_interL" + | Int_nl_carrier "('f, int) poly_inter_list" + | Rat_carrier "('f, rat) lpoly_interL" + | Rat_nl_carrier rat "('f, rat) poly_inter_list" + | Real_carrier "('f, real) lpoly_interL" + | Real_nl_carrier real "('f, real) poly_inter_list" + | Arctic_carrier "('f, arctic) lpoly_interL" + | Arctic_rat_carrier "('f, rat arctic_delta) lpoly_interL" + | Int_mat_carrier nat nat "('f, int mat) lpoly_interL" + | Rat_mat_carrier nat nat "('f, rat mat) lpoly_interL" + | Real_mat_carrier nat nat "('f, real mat) lpoly_interL" + | Arctic_mat_carrier nat "('f, arctic mat) lpoly_interL" + | Arctic_rat_mat_carrier nat "('f, rat arctic_delta mat) lpoly_interL" + | RPO "'f status_prec_repr" "'f afs_list" + | KBO "'f prec_weight_repr" "'f afs_list" + +datatype_new list_order_type = MS_Ext | Max_Ext | Min_Ext | Dms_Ext +type_synonym 'f scnp_af = "(('f \<times> nat) \<times> (nat \<times> nat) list) list" + +datatype_new 'f root_redtriple_impl = SCNP list_order_type "'f scnp_af" "'f redtriple_impl" + +type_synonym 'f sig_map_list = "(('f \<times> nat) \<times> 'f list) list" +type_synonym ('f,'v) uncurry_info = "'f \<times> 'f sig_map_list \<times> ('f,'v)rules \<times> ('f,'v)rules" + +datatype_new arithFun = + Arg nat +| Const nat +| Sum "arithFun list" +| Max "arithFun list" +| Min "arithFun list" +| Prod "arithFun list" +| IfEqual arithFun arithFun arithFun arithFun + +datatype_new 'f sl_inter = SL_Inter nat "(('f \<times> nat) \<times> arithFun) list" +datatype_new ('f,'v)sl_variant = Rootlab "('f \<times> nat) option" | Finitelab "'f sl_inter" | QuasiFinitelab "'f sl_inter" 'v + +type_synonym ('f,'v)crit_pair_joins = "(('f,'v)term \<times> ('f,'v)rseq \<times> ('f,'v)term \<times> ('f,'v)rseq)list" +datatype_new 'f join_info = Guided "('f,string)crit_pair_joins" | Join_NF | Join_BFS nat + +type_synonym unknown_info = string + +type_synonym dummy_prf = unit + + +datatype_new ('f,'v)complex_constant_removal_prf = Complex_Constant_Removal_Proof + "('f,'v)term" + "(('f,'v)rule \<times> ('f,'v)rule) list" + +datatype_new ('f,'v)cond_constraint + = CC_cond bool "('f,'v)rule" + | CC_rewr "('f,'v)term" "('f,'v)term" + | CC_impl "('f,'v)cond_constraint list" "('f,'v)cond_constraint" + | CC_all 'v "('f,'v)cond_constraint" + +type_synonym ('f, 'v, 'w) gsubstL = "('v \<times> ('f, 'w) term) list" +type_synonym ('f, 'v) substL = "('f, 'v, 'v) gsubstL" + +datatype_new ('f,'v)cond_constraint_prf = + Final +| Delete_Condition "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf" +| Different_Constructor "('f,'v)cond_constraint" +| Same_Constructor "('f,'v)cond_constraint" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf" +| Variable_Equation 'v "('f,'v)term" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf" +| Funarg_Into_Var "('f,'v)cond_constraint" nat 'v "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf" +| Simplify_Condition "('f,'v)cond_constraint" "('f,'v)substL" "('f,'v)cond_constraint" "('f,'v)cond_constraint_prf" +| 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" + + +datatype_new ('f,'v)cond_red_pair_prf = Cond_Red_Pair_Prf + 'f + "(('f,'v)cond_constraint \<times> ('f,'v)rules \<times> ('f,'v)cond_constraint_prf) list" + nat + nat + +datatype_new ('q,'f)ta_rule = TA_rule 'f "'q list" 'q ("_ _ \<rightarrow> _") +datatype_new ('q,'f)tree_automaton = Tree_Automaton "'q list" "('q,'f)ta_rule list" "('q \<times> 'q)list" +datatype_new 'q ta_relation = Decision_Proc | Id_Relation | Some_Relation "('q \<times> 'q) list" + +datatype_new boundstype = Roof | Match +datatype_new ('f,'q)bounds_info = Bounds_Info boundstype nat "'q list" "('q, 'f \<times> nat) tree_automaton" "'q ta_relation" + +datatype_new ('f, 'v) pat_eqv_prf = + Pat_Dom_Renaming "('f, 'v) substL" +| Pat_Irrelevant "('f, 'v) substL" "('f, 'v) substL" +| Pat_Simplify "('f, 'v) substL" "('f, 'v) substL" + +datatype_new pat_rule_pos = Pat_Base | Pat_Pump | Pat_Close + +datatype_new ('f, 'v) pat_rule_prf = + Pat_OrigRule "('f, 'v) rule" bool +| Pat_InitPump "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" +| Pat_InitPumpCtxt "('f, 'v) pat_rule_prf" "('f, 'v) substL" pos 'v +| Pat_Equiv "('f, 'v) pat_rule_prf" bool "('f, 'v) pat_eqv_prf" +| Pat_Narrow "('f, 'v) pat_rule_prf" "('f, 'v) pat_rule_prf" pos +| Pat_Inst "('f, 'v) pat_rule_prf" "('f, 'v) substL" pat_rule_pos +| Pat_Rewr "('f, 'v) pat_rule_prf" "('f, 'v) term \<times> ('f, 'v) rseq" pat_rule_pos 'v +| Pat_Exp_Sigma "('f, 'v) pat_rule_prf" nat + +datatype_new ('f, 'v) non_loop_prf = + Non_Loop_Prf "('f, 'v) pat_rule_prf" "('f, 'v) substL" "('f, 'v) substL" nat nat pos + + +datatype_new ('f, 'l, 'v) problem = + SN_TRS "('f,'l,'v)qreltrsLL" +| SN_FP_TRS "('f,'l,'v)fptrsLL" +| Finite_DPP "('f,'l,'v) dppLL" +| Unknown_Problem unknown_info +| Not_SN_TRS "('f,'l,'v)qtrsLL" +| Not_RelSN_TRS "('f,'l,'v)qreltrsLL" +| Infinite_DPP "('f,'l,'v) dppLL" +| Not_SN_FP_TRS "('f,'l,'v)fptrsLL" +declare [[bnf_timing]] +datatype_new ('f, 'l, 'v, 'a, 'b, 'c, 'd, 'e) generic_assm_proof = + SN_assm_proof "('f,'l,'v)qreltrsLL" 'a +| Finite_assm_proof "('f,'l,'v)dppLL" 'b +| SN_FP_assm_proof "('f,'l,'v)fptrsLL" 'c +| Not_SN_assm_proof "('f,'l,'v)qtrsLL" 'a +| Infinite_assm_proof "('f,'l,'v)dppLL" 'b +| Not_RelSN_assm_proof "('f,'l,'v)qreltrsLL" 'c +| Not_SN_FP_assm_proof "('f,'l,'v)fptrsLL" 'd +| Unknown_assm_proof unknown_info 'e + +type_synonym ('f,'l,'v,'a,'b,'c,'d)assm_proof = "('f,'l,'v,'a,'b,'c,dummy_prf,'d)generic_assm_proof" + +datatype_new ('f, 'l, 'v) assm = + SN_assm "('f,'l,'v)problem list" "('f,'l,'v)qreltrsLL" +| SN_FP_assm "('f,'l,'v)problem list" "('f,'l,'v)fptrsLL" +| Finite_assm "('f,'l,'v)problem list" "('f,'l,'v)dppLL" +| Unknown_assm "('f,'l,'v)problem list" unknown_info +| Not_SN_assm "('f,'l,'v)problem list" "('f,'l,'v)qtrsLL" +| Not_RelSN_assm "('f,'l,'v)problem list" "('f,'l,'v)qreltrsLL" +| Not_SN_FP_assm "('f,'l,'v)problem list" "('f,'l,'v)fptrsLL" +| Infinite_assm "('f,'l,'v)problem list" "('f,'l,'v)dppLL" + +fun satisfied :: "('f,'l,'v)problem \<Rightarrow> bool" where + "satisfied (SN_TRS t) = (t = t)" +| "satisfied (SN_FP_TRS t) = (t \<noteq> t)" +| "satisfied (Finite_DPP d) = (d \<noteq> d)" +| "satisfied (Unknown_Problem s) = (s = ''foo'')" +| "satisfied (Not_SN_TRS (nfs,q,r)) = (length q = length r)" +| "satisfied (Not_RelSN_TRS (nfs,q,r,rw)) = (r = rw)" +| "satisfied (Infinite_DPP d) = (d = d)" +| "satisfied (Not_SN_FP_TRS t) = (t = t)" + +fun collect_assms :: "('tp \<Rightarrow> ('f,'l,'v) assm list) + \<Rightarrow> ('dpp \<Rightarrow> ('f,'l,'v) assm list) + \<Rightarrow> ('fptp \<Rightarrow> ('f,'l,'v) assm list) + \<Rightarrow> ('unk \<Rightarrow> ('f,'l,'v) assm list) + \<Rightarrow> ('f,'l,'v,'tp,'dpp,'fptp,'unk) assm_proof \<Rightarrow> ('f,'l,'v) assm list" where + "collect_assms tp dpp fptp unk (SN_assm_proof t prf) = tp prf" +| "collect_assms tp dpp fptp unk (SN_FP_assm_proof t prf) = fptp prf" +| "collect_assms tp dpp fptp unk (Finite_assm_proof d prf) = dpp prf" +| "collect_assms tp dpp fptp unk (Unknown_assm_proof p prf) = unk prf" +| "collect_assms _ _ _ _ _ = []" + +fun collect_neg_assms :: "('tp \<Rightarrow> ('f,'l,'v) assm list) + \<Rightarrow> ('dpp \<Rightarrow> ('f,'l,'v) assm list) + \<Rightarrow> ('rtp \<Rightarrow> ('f,'l,'v) assm list) + \<Rightarrow> ('fptp \<Rightarrow> ('f,'l,'v) assm list) + \<Rightarrow> ('unk \<Rightarrow> ('f,'l,'v) assm list) + \<Rightarrow> ('f,'l,'v,'tp,'dpp,'rtp,'fptp,'unk) generic_assm_proof \<Rightarrow> ('f,'l,'v) assm list" where + "collect_neg_assms tp dpp rtp fptp unk (Not_SN_assm_proof t prf) = tp prf" +| "collect_neg_assms tp dpp rtp fptp unk (Infinite_assm_proof d prf) = dpp prf" +| "collect_neg_assms tp dpp rtp fptp unk (Not_RelSN_assm_proof t prf) = rtp prf" +| "collect_neg_assms tp dpp rtp fptp unk (Not_SN_FP_assm_proof t prf) = fptp prf" +| "collect_neg_assms tp dpp rtp fptp unk (Unknown_assm_proof p prf) = unk prf" +| "collect_neg_assms tp dpp rtp fptp unk _ = []" + + + +datatype_new ('f, 'l, 'v) dp_nontermination_proof = + DP_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) prseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt" +| DP_Nonloop "(('f,'l)lab, 'v)non_loop_prf" +| DP_Rule_Removal "('f,'l,'v)trsLL option" "('f,'l,'v)trsLL option" "('f,'l,'v) dp_nontermination_proof" +| DP_Q_Increase "('f,'l,'v)termsLL" "('f,'l,'v) dp_nontermination_proof" +| DP_Q_Reduction "('f,'l,'v)termsLL" "('f,'l,'v) dp_nontermination_proof" +| DP_Termination_Switch "('f,'l)lab join_info" "('f,'l,'v) dp_nontermination_proof" +| DP_Instantiation "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof" +| 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" +| DP_Narrowing "('f,'l,'v)ruleLL" pos "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof" +| DP_Assume_Infinite "('f, 'l, 'v) dppLL" + "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof, + ('f, 'l, 'v) dp_nontermination_proof, + ('f, 'l, 'v) reltrs_nontermination_proof, + ('f, 'l, 'v) fp_nontermination_proof, + ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list" + and +('f,'l,'v) "trs_nontermination_proof" = + TRS_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) rseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt" +| TRS_Not_Well_Formed +| TRS_Rule_Removal "('f,'l,'v)trsLL" "('f,'l,'v) trs_nontermination_proof" +| TRS_String_Reversal "('f,'l,'v) trs_nontermination_proof" +| TRS_DP_Trans "('f,'l,'v)trsLL" "('f,'l,'v) dp_nontermination_proof" +| TRS_Nonloop "(('f,'l)lab,'v) non_loop_prf" +| TRS_Q_Increase "('f,'l,'v)termsLL" "('f,'l,'v) trs_nontermination_proof" +| TRS_Assume_Not_SN "('f, 'l, 'v)qtrsLL" + "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof, + ('f, 'l, 'v) dp_nontermination_proof, + ('f, 'l, 'v) reltrs_nontermination_proof, + ('f, 'l, 'v) fp_nontermination_proof, + ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list" + and +('f,'l,'v)"reltrs_nontermination_proof" = + Rel_Loop "(('f,'l)lab,'v) term" "(('f,'l)lab, 'v) prseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt" +| Rel_Not_Well_Formed +| Rel_Rule_Removal "('f,'l,'v)trsLL option" "('f,'l,'v)trsLL option" "('f,'l,'v) reltrs_nontermination_proof" +| Rel_R_Not_SN "('f,'l,'v) trs_nontermination_proof" +| Rel_TRS_Assume_Not_SN "('f, 'l, 'v)qreltrsLL" + "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof, + ('f, 'l, 'v) dp_nontermination_proof, + ('f, 'l, 'v) reltrs_nontermination_proof, + ('f, 'l, 'v) fp_nontermination_proof, + ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list" + and + ('f, 'l, 'v) "fp_nontermination_proof" = + FPTRS_Loop "(('f,'l)lab, 'v) term" "(('f,'l)lab, 'v) rseq" "(('f,'l)lab, 'v) substL" "(('f,'l)lab, 'v) ctxt" +| FPTRS_Rule_Removal "('f,'l,'v)trsLL" "('f,'l,'v) fp_nontermination_proof" +| FPTRS_Assume_Not_SN "('f, 'l, 'v)fptrsLL" + "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof, + ('f, 'l, 'v) dp_nontermination_proof, + ('f, 'l, 'v) reltrs_nontermination_proof, + ('f, 'l, 'v) fp_nontermination_proof, + ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list" + and + ('f, 'l, 'v) neg_unknown_proof = + Assume_NT_Unknown unknown_info + "('f,'l,'v,('f, 'l, 'v) trs_nontermination_proof, + ('f, 'l, 'v) dp_nontermination_proof, + ('f, 'l, 'v) reltrs_nontermination_proof, + ('f, 'l, 'v) fp_nontermination_proof, + ('f, 'l, 'v) neg_unknown_proof) generic_assm_proof list" + + +datatype_new ('f, 'l, 'v) dp_termination_proof = + P_is_Empty +| Subterm_Criterion_Proc "('f, 'l) lab projL" "('f, 'l, 'v) rseqL" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Redpair_Proc "('f,'l)lab root_redtriple_impl + ('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Redpair_UR_Proc "('f, 'l) lab root_redtriple_impl + ('f, 'l) lab redtriple_impl" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Usable_Rules_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Dep_Graph_Proc "(('f, 'l, 'v) dp_termination_proof option \<times> ('f, 'l, 'v) trsLL) list" +| Mono_Redpair_Proc "('f, 'l) lab redtriple_impl" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Mono_Redpair_UR_Proc "('f, 'l) lab redtriple_impl" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Size_Change_Subterm_Proc "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list" +| Size_Change_Redpair_Proc "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL option" + "((('f, 'l) lab, 'v) rule \<times> ((nat \<times> nat) list \<times> (nat \<times> nat) list)) list" +| Uncurry_Proc "nat option" "(('f, 'l) lab, 'v) uncurry_info" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Fcc_Proc "('f, 'l) lab" "(('f, 'l) lab, 'v) ctxt list" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Split_Proc + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" + "('f, 'l, 'v) dp_termination_proof" "('f, 'l, 'v) dp_termination_proof" +| Semlab_Proc + "(('f, 'l) lab, 'v) sl_variant" "('f, 'l, 'v) trsLL" + "(('f, 'l) lab, 'v) term list" "('f, 'l, 'v) trsLL" + "('f, 'l, 'v) dp_termination_proof" +| Switch_Innermost_Proc "('f, 'l) lab join_info" "('f, 'l, 'v) dp_termination_proof" +| Rewriting_Proc + "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" + "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) dp_termination_proof" +| Instantiation_Proc "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Forward_Instantiation_Proc + "('f, 'l, 'v) ruleLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL option" "('f, 'l, 'v) dp_termination_proof" +| Narrowing_Proc "('f, 'l, 'v) ruleLL" pos "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Assume_Finite + "('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" +| Unlab_Proc "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) dp_termination_proof" +| Q_Reduction_Proc "('f, 'l, 'v) termsLL" "('f, 'l, 'v) dp_termination_proof" +| Complex_Constant_Removal_Proc "(('f,'l)lab,'v)complex_constant_removal_prf" "('f, 'l, 'v) dp_termination_proof" +| General_Redpair_Proc + "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trsLL" + "(('f, 'l) lab, 'v) cond_red_pair_prf" "('f, 'l, 'v) dp_termination_proof list" +| To_Trs_Proc "('f, 'l, 'v) trs_termination_proof" +and ('f, 'l, 'v) trs_termination_proof = + DP_Trans bool bool "(('f, 'l) lab, 'v) rules" "('f, 'l, 'v) dp_termination_proof" +| Rule_Removal "('f, 'l) lab redtriple_impl" "('f, 'l, 'v) trsLL" "('f, 'l, 'v)trs_termination_proof" +| String_Reversal "('f, 'l, 'v) trs_termination_proof" +| Bounds "(('f, 'l) lab, 'v) bounds_info" +| Uncurry "(('f, 'l) lab, 'v) uncurry_info" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" +| Semlab + "(('f, 'l) lab, 'v) sl_variant" "(('f, 'l) lab, 'v) term list" + "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" +| R_is_Empty +| Fcc "(('f, 'l) lab, 'v) ctxt list" "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" +| Split "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" "('f, 'l, 'v) trs_termination_proof" +| Switch_Innermost "('f, 'l) lab join_info" "('f, 'l, 'v) trs_termination_proof" +| Drop_Equality "('f, 'l, 'v) trs_termination_proof" +| Remove_Nonapplicable_Rules "('f, 'l, 'v) trsLL" "('f, 'l, 'v) trs_termination_proof" +| 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" +and ('f, 'l, 'v) unknown_proof = + 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" +and ('f, 'l, 'v) fptrs_termination_proof = + 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" + + +end
--- a/src/HOL/ROOT Mon Jul 21 17:57:16 2014 +0200 +++ b/src/HOL/ROOT Tue Jul 22 08:07:47 2014 +0200 @@ -734,6 +734,8 @@ Misc_Datatype Misc_Primcorec Misc_Primrec + theories [condition = ISABELLE_FULL_TEST] + IsaFoR_Datatypes session "HOL-Word" (main) in Word = HOL + options [document_graph]
--- a/src/Pure/General/completion.scala Mon Jul 21 17:57:16 2014 +0200 +++ b/src/Pure/General/completion.scala Tue Jul 22 08:07: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 17:57:16 2014 +0200 +++ b/src/Pure/PIDE/markup.ML Tue Jul 22 08:07: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 17:57:16 2014 +0200 +++ b/src/Pure/PIDE/markup.scala Tue Jul 22 08:07: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 17:57:16 2014 +0200 +++ b/src/Pure/Tools/simplifier_trace.ML Tue Jul 22 08:07: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 17:57:16 2014 +0200 +++ b/src/Pure/Tools/simplifier_trace.scala Tue Jul 22 08:07: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 17:57:16 2014 +0200 +++ b/src/Tools/jEdit/src/active.scala Tue Jul 22 08:07: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 17:57:16 2014 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Tue Jul 22 08:07: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 17:57:16 2014 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Tue Jul 22 08:07: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 17:57:16 2014 +0200 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Jul 22 08:07: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) }