# HG changeset patch # User hoelzl # Date 1277223344 -7200 # Node ID 9de1add14bac1fb496481415608be53935f3b833 # Parent 44e42d392c6eea3b353d9a1ef3f79fad9ad0c7ed# Parent a5aa61b7fa740aca8fea0d49bc421ef116c2e6b7 merged diff -r 44e42d392c6e -r 9de1add14bac .hgtags --- a/.hgtags Mon Jun 21 19:33:51 2010 +0200 +++ b/.hgtags Tue Jun 22 18:15:44 2010 +0200 @@ -25,5 +25,4 @@ fc385ce6187d5ad2cef90f1e6240cc691e02d827 Isabelle2005 5c8618f95d240046bbbb609b643c06704888f587 Isabelle2009 6a973bd4394996c31f638e5c59ea6bb953335c9a Isabelle2009-1 -935c75359742ccfd4abba0c33a440241e6ef2b1e isa2009-2-test0 -d1cdbc7524b619815236e8e2e61e36809ee2d338 isa2009-2-test1 +35815ce9218a8822a50f5d80b96aa8d1970ec35d Isabelle2009-2 diff -r 44e42d392c6e -r 9de1add14bac Admin/CHECKLIST --- a/Admin/CHECKLIST Mon Jun 21 19:33:51 2010 +0200 +++ b/Admin/CHECKLIST Tue Jun 22 18:15:44 2010 +0200 @@ -15,7 +15,7 @@ - Admin/update-keywords; -- check ANNOUNCE, README, INSTALL, NEWS, COPYRIGHT, CONTRIBUTORS; +- check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS; - diff NEWS wrt. last official release, which is read-only; diff -r 44e42d392c6e -r 9de1add14bac Admin/makebundle --- a/Admin/makebundle Mon Jun 21 19:33:51 2010 +0200 +++ b/Admin/makebundle Tue Jun 22 18:15:44 2010 +0200 @@ -66,7 +66,7 @@ HEAPS_ARCHIVE="$ARCHIVE_DIR/${ISABELLE_NAME}_heaps_${PLATFORM}.tar.gz" [ -f "$HEAPS_ARCHIVE" ] || fail "Bad heaps archive: $HEAPS_ARCHIVE" echo "heaps" -tar -C "$ISABELLE_HOME" -x -z -f "$HEAPS_ARCHIVE" +tar -C "$TMP" -x -z -f "$HEAPS_ARCHIVE" BUNDLE_ARCHIVE="${ARCHIVE_DIR}/${ISABELLE_NAME}_bundle_${PLATFORM}.tar.gz" diff -r 44e42d392c6e -r 9de1add14bac Admin/makedist --- a/Admin/makedist Mon Jun 21 19:33:51 2010 +0200 +++ b/Admin/makedist Tue Jun 22 18:15:44 2010 +0200 @@ -145,11 +145,14 @@ rm -rf doc-src mkdir -p contrib +cat >contrib/README < (nat * nat) => bool" + intrel :: "(nat * nat) => (nat * nat) => bool" where "intrel (x, y) (u, v) = (x + v = u + y)" - quotient_type int = "nat × nat" / intrel + quotient_type int = "nat * nat" / intrel by (auto simp add: equivp_def expand_fun_eq) - + quotient_definition "0::int" is "(0::nat, 0::nat)" @@ -292,6 +292,8 @@ * Theory PReal, including the type "preal" and related operations, has been removed. INCOMPATIBILITY. +* Real: new development using Cauchy Sequences. + * Split off theory "Big_Operators" containing setsum, setprod, Inf_fin, Sup_fin, Min, Max from theory Finite_Set. INCOMPATIBILITY. @@ -511,6 +513,17 @@ "sharing_depth", and "show_skolems" options. INCOMPATIBILITY. - Removed "nitpick_intro" attribute. INCOMPATIBILITY. +* Method "induct" now takes instantiations of the form t, where t is not + a variable, as a shorthand for "x == t", where x is a fresh variable. + If this is not intended, t has to be enclosed in parentheses. + By default, the equalities generated by definitional instantiations + are pre-simplified, which may cause parameters of inductive cases + to disappear, or may even delete some of the inductive cases. + Use "induct (no_simp)" instead of "induct" to restore the old + behaviour. The (no_simp) option is also understood by the "cases" + and "nominal_induct" methods, which now perform pre-simplification, too. + INCOMPATIBILITY. + *** HOLCF *** @@ -683,6 +696,13 @@ See src/Tools/jEdit or "isabelle jedit" provided by the properly built component. +* "IsabelleText" is a Unicode font derived from Bitstream Vera Mono +and Bluesky TeX fonts. It provides the usual Isabelle symbols, +similar to the default assignment of the document preparation system +(cf. isabellesym.sty). The Isabelle/Scala class Isabelle_System +provides some operations for direct access to the font without asking +the user for manual installation. + New in Isabelle2009-1 (December 2009) @@ -3410,8 +3430,6 @@ * Real: proper support for ML code generation, including 'quickcheck'. Reals are implemented as arbitrary precision rationals. -* Real: new development using Cauchy Sequences. - * Hyperreal: Several constants that previously worked only for the reals have been generalized, so they now work over arbitrary vector spaces. Type annotations may need to be added in some cases; potential diff -r 44e42d392c6e -r 9de1add14bac README --- a/README Mon Jun 21 19:33:51 2010 +0200 +++ b/README Tue Jun 22 18:15:44 2010 +0200 @@ -21,10 +21,9 @@ Installation - Binary packages are available for Isabelle/HOL etc. for several - platforms from the Isabelle web page. The system may be also built - from scratch, using the tar.gz source distribution. See file - INSTALL as distributed with Isabelle for more information. + Completely integrated bundles including the full Isabelle sources, + documentation, add-on tools and precompiled logic images for + several platforms are available from the Isabelle web page. Further background information may be found in the Isabelle System Manual, distributed with the sources (directory doc). diff -r 44e42d392c6e -r 9de1add14bac doc-src/IsarRef/Thy/Proof.thy --- a/doc-src/IsarRef/Thy/Proof.thy Mon Jun 21 19:33:51 2010 +0200 +++ b/doc-src/IsarRef/Thy/Proof.thy Tue Jun 22 18:15:44 2010 +0200 @@ -1277,16 +1277,16 @@ ``strengthened'' inductive statements within the object-logic. \begin{rail} - 'cases' (insts * 'and') rule? + 'cases' '(no_simp)'? (insts * 'and') rule? ; - 'induct' (definsts * 'and') \\ arbitrary? taking? rule? + 'induct' '(no_simp)'? (definsts * 'and') \\ arbitrary? taking? rule? ; 'coinduct' insts taking rule? ; rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +) ; - definst: name ('==' | equiv) term | inst + definst: name ('==' | equiv) term | '(' term ')' | inst ; definsts: ( definst *) ; @@ -1320,7 +1320,9 @@ of premises of the case rule; within each premise, the \emph{prefix} of variables is instantiated. In most situations, only a single term needs to be specified; this refers to the first variable of the - last premise (it is usually the same for all cases). + last premise (it is usually the same for all cases). The @{text + "(no_simp)"} option can be used to disable pre-simplification of + cases (see the description of @{method induct} below for details). \item @{method induct}~@{text "insts R"} is analogous to the @{method cases} method, but refers to induction rules, which are @@ -1342,15 +1344,28 @@ present in the induction rule. This enables the writer to specify only induction variables, or both predicates and variables, for example. - + Instantiations may be definitional: equations @{text "x \ t"} introduce local definitions, which are inserted into the claim and discharged after applying the induction rule. Equalities reappear in the inductive cases, but have been transformed according to the induction principle being involved here. In order to achieve practically useful induction hypotheses, some variables occurring in - @{text t} need to be fixed (see below). - + @{text t} need to be fixed (see below). Instantiations of the form + @{text t}, where @{text t} is not a variable, are taken as a + shorthand for \mbox{@{text "x \ t"}}, where @{text x} is a fresh + variable. If this is not intended, @{text t} has to be enclosed in + parentheses. By default, the equalities generated by definitional + instantiations are pre-simplified using a specific set of rules, + usually consisting of distinctness and injectivity theorems for + datatypes. This pre-simplification may cause some of the parameters + of an inductive case to disappear, or may even completely delete + some of the inductive cases, if one of the equalities occurring in + their premises can be simplified to @{text False}. The @{text + "(no_simp)"} option can be used to disable pre-simplification. + Additional rules to be used in pre-simplification can be declared + using the @{attribute_def induct_simp} attribute. + The optional ``@{text "arbitrary: x\<^sub>1 \ x\<^sub>m"}'' specification generalizes variables @{text "x\<^sub>1, \, x\<^sub>m"} of the original goal before applying induction. Thus diff -r 44e42d392c6e -r 9de1add14bac doc-src/IsarRef/Thy/document/Proof.tex --- a/doc-src/IsarRef/Thy/document/Proof.tex Mon Jun 21 19:33:51 2010 +0200 +++ b/doc-src/IsarRef/Thy/document/Proof.tex Tue Jun 22 18:15:44 2010 +0200 @@ -1275,16 +1275,16 @@ ``strengthened'' inductive statements within the object-logic. \begin{rail} - 'cases' (insts * 'and') rule? + 'cases' '(no_simp)'? (insts * 'and') rule? ; - 'induct' (definsts * 'and') \\ arbitrary? taking? rule? + 'induct' '(no_simp)'? (definsts * 'and') \\ arbitrary? taking? rule? ; 'coinduct' insts taking rule? ; rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +) ; - definst: name ('==' | equiv) term | inst + definst: name ('==' | equiv) term | '(' term ')' | inst ; definsts: ( definst *) ; @@ -1317,7 +1317,8 @@ of premises of the case rule; within each premise, the \emph{prefix} of variables is instantiated. In most situations, only a single term needs to be specified; this refers to the first variable of the - last premise (it is usually the same for all cases). + last premise (it is usually the same for all cases). The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} option can be used to disable pre-simplification of + cases (see the description of \hyperlink{method.induct}{\mbox{\isa{induct}}} below for details). \item \hyperlink{method.induct}{\mbox{\isa{induct}}}~\isa{{\isachardoublequote}insts\ R{\isachardoublequote}} is analogous to the \hyperlink{method.cases}{\mbox{\isa{cases}}} method, but refers to induction rules, which are @@ -1339,15 +1340,27 @@ present in the induction rule. This enables the writer to specify only induction variables, or both predicates and variables, for example. - + Instantiations may be definitional: equations \isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}} introduce local definitions, which are inserted into the claim and discharged after applying the induction rule. Equalities reappear in the inductive cases, but have been transformed according to the induction principle being involved here. In order to achieve practically useful induction hypotheses, some variables occurring in - \isa{t} need to be fixed (see below). - + \isa{t} need to be fixed (see below). Instantiations of the form + \isa{t}, where \isa{t} is not a variable, are taken as a + shorthand for \mbox{\isa{{\isachardoublequote}x\ {\isasymequiv}\ t{\isachardoublequote}}}, where \isa{x} is a fresh + variable. If this is not intended, \isa{t} has to be enclosed in + parentheses. By default, the equalities generated by definitional + instantiations are pre-simplified using a specific set of rules, + usually consisting of distinctness and injectivity theorems for + datatypes. This pre-simplification may cause some of the parameters + of an inductive case to disappear, or may even completely delete + some of the inductive cases, if one of the equalities occurring in + their premises can be simplified to \isa{False}. The \isa{{\isachardoublequote}{\isacharparenleft}no{\isacharunderscore}simp{\isacharparenright}{\isachardoublequote}} option can be used to disable pre-simplification. + Additional rules to be used in pre-simplification can be declared + using the \indexdef{}{attribute}{induct\_simp}\hypertarget{attribute.induct-simp}{\hyperlink{attribute.induct-simp}{\mbox{\isa{induct{\isacharunderscore}simp}}}} attribute. + The optional ``\isa{{\isachardoublequote}arbitrary{\isacharcolon}\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub m{\isachardoublequote}}'' specification generalizes variables \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub m{\isachardoublequote}} of the original goal before applying induction. Thus induction hypotheses may become sufficiently general to get the diff -r 44e42d392c6e -r 9de1add14bac doc-src/Ref/introduction.tex --- a/doc-src/Ref/introduction.tex Mon Jun 21 19:33:51 2010 +0200 +++ b/doc-src/Ref/introduction.tex Tue Jun 22 18:15:44 2010 +0200 @@ -5,9 +5,7 @@ \index{starting up|bold}\nobreak % We assume that your local Isabelle administrator (this might be you!) has -already installed the Isabelle system together with appropriate object-logics ---- otherwise see the \texttt{README} and \texttt{INSTALL} files in the -top-level directory of the distribution on how to do this. +already installed the Isabelle system together with appropriate object-logics. \medskip Let $\langle isabellehome \rangle$ denote the location where the distribution has been installed. To run Isabelle from a the shell diff -r 44e42d392c6e -r 9de1add14bac src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Jun 21 19:33:51 2010 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Jun 22 18:15:44 2010 +0200 @@ -5284,7 +5284,7 @@ (* class constraint due to continuous_on_inverse *) shows "compact s \ continuous_on s f \ (f ` s = t) \ inj_on f s \ s homeomorphic t" - unfolding homeomorphic_def by(auto intro: homeomorphism_compact) + unfolding homeomorphic_def by (metis homeomorphism_compact) text{* Preservation of topological properties. *} diff -r 44e42d392c6e -r 9de1add14bac src/HOL/Nominal/Examples/CK_Machine.thy --- a/src/HOL/Nominal/Examples/CK_Machine.thy Mon Jun 21 19:33:51 2010 +0200 +++ b/src/HOL/Nominal/Examples/CK_Machine.thy Tue Jun 22 18:15:44 2010 +0200 @@ -491,11 +491,11 @@ and b: "\ \ e' : T'" shows "(\@\) \ e[x::=e'] : T" using a b -proof (nominal_induct \'\"\@[(x,T')]@\" e T avoiding: x e' \ rule: typing.strong_induct) +proof (nominal_induct "\@[(x,T')]@\" e T avoiding: x e' \ rule: typing.strong_induct) case (t_VAR y T x e' \) then have a1: "valid (\@[(x,T')]@\)" and a2: "(y,T) \ set (\@[(x,T')]@\)" - and a3: "\ \ e' : T'" by simp_all + and a3: "\ \ e' : T'" . from a1 have a4: "valid (\@\)" by (rule valid_insert) { assume eq: "x=y" from a1 a2 have "T=T'" using eq by (auto intro: context_unique) diff -r 44e42d392c6e -r 9de1add14bac src/HOL/Nominal/Examples/Type_Preservation.thy --- a/src/HOL/Nominal/Examples/Type_Preservation.thy Mon Jun 21 19:33:51 2010 +0200 +++ b/src/HOL/Nominal/Examples/Type_Preservation.thy Tue Jun 22 18:15:44 2010 +0200 @@ -141,11 +141,11 @@ and b: "\ \ e' : T'" shows "(\@\) \ e[x::=e'] : T" using a b -proof (nominal_induct \'\"\@[(x,T')]@\" e T avoiding: x e' \ rule: typing.strong_induct) +proof (nominal_induct "\@[(x,T')]@\" e T avoiding: x e' \ rule: typing.strong_induct) case (t_Var y T x e' \) then have a1: "valid (\@[(x,T')]@\)" and a2: "(y,T) \ set (\@[(x,T')]@\)" - and a3: "\ \ e' : T'" by simp_all + and a3: "\ \ e' : T'" . from a1 have a4: "valid (\@\)" by (rule valid_insert) { assume eq: "x=y" from a1 a2 have "T=T'" using eq by (auto intro: context_unique) diff -r 44e42d392c6e -r 9de1add14bac src/HOL/Nominal/INSTALL --- a/src/HOL/Nominal/INSTALL Mon Jun 21 19:33:51 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,57 +0,0 @@ - -Installation Notes for the Nominal Datatype Package -=================================================== - -Although the nominal datatype package is an official -package in the development snapshot of Isabelle, we -keep a semi-official snapshot of Isabelle and Nominal -under - - http://isabelle.in.tum.de/nominal/ - -This snapshot contains the latest stable release of the -nominal datatype package. - -To install it, follow the instructions of Isabelle's INSTALL -about how a snap-shot can be set up. The building process -needs to be started inside the [ISABELLE_HOME] directory with -the command: - - ./build -m HOL-Nominal - -After the build completes, install the files with the command - - ./bin/isabelle install -p /usr/local/bin - -where /usr/local/bin needs to be replaced by an appropriate -directory, if you are not root on the system. - -The sources of the nominal datatype package can be found -in the directory - - [ISABELLE_HOME]/src/HOL/Nominal - -The examples are in - - [ISABELLE_HOME]/src/HOL/Nominal/Examples - -Starting Isabelle with the Nominal Datatype Package Preloaded -============================================================= - -Isabelle and the Proof-General interface can be started -with - - Isabelle -L HOL-Nominal <> & - -on the command-line. This automatically loads the correct -keyword file needed for the nominal datatype package. - -Problems with starting Isabelle and Proof-General usually -come from old versions of Proof-General. So make sure you -have installed at least the version ProofGeneral-3.6pre050930. - -If you have problems or comments about the installation process, -please make use of the nominal mailing list at - -https://mailmanbroy.informatik.tu-muenchen.de/pipermail/nominal-isabelle/ - diff -r 44e42d392c6e -r 9de1add14bac src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Mon Jun 21 19:33:51 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jun 22 18:15:44 2010 +0200 @@ -874,7 +874,7 @@ end | Cst (cst, T, _) => if cst = Unknown orelse cst = Unrep then - case (is_boolean_type T, polar) of + case (is_boolean_type T, polar |> unsound ? flip_polarity) of (true, Pos) => Cst (False, T, Formula Pos) | (true, Neg) => Cst (True, T, Formula Neg) | _ => Cst (cst, T, best_opt_set_rep_for_type scope T) diff -r 44e42d392c6e -r 9de1add14bac src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Mon Jun 21 19:33:51 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Tue Jun 22 18:15:44 2010 +0200 @@ -137,7 +137,7 @@ fun mk_skolem_id t = let val T = fastype_of t in - Const (@{const_name skolem_id}, T --> T) $ Envir.beta_eta_contract t + Const (@{const_name skolem_id}, T --> T) $ Envir.beta_norm t end (*Traverse a theorem, accumulating Skolem function definitions.*) @@ -409,6 +409,7 @@ val ctxt0 = Variable.global_thm_context th val (nnfth, ctxt) = to_nnf th ctxt0 val inline = exists_type (exists_subtype (can dest_TFree)) (prop_of nnfth) + val inline = false (* FIXME: temporary *) val defs = skolem_theorems_of_assume inline s nnfth val (cnfs, ctxt) = Meson.make_cnf defs nnfth ctxt in @@ -446,7 +447,7 @@ (**** Translate a set of theorems into CNF ****) -fun pair_name_cls k (n, []) = [] +fun pair_name_cls _ (_, []) = [] | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss) (*The combination of rev and tail recursion preserves the original order*) diff -r 44e42d392c6e -r 9de1add14bac src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Mon Jun 21 19:33:51 2010 +0200 +++ b/src/Pure/General/pretty.scala Tue Jun 22 18:15:44 2010 +0200 @@ -134,7 +134,7 @@ def string_of(input: List[XML.Tree], margin: Int = margin_default, metric: String => Double = metric_default): String = - formatted(input).iterator.flatMap(XML.content).mkString + formatted(input, margin, metric).iterator.flatMap(XML.content).mkString /* unformatted output */ diff -r 44e42d392c6e -r 9de1add14bac src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Mon Jun 21 19:33:51 2010 +0200 +++ b/src/Pure/Isar/runtime.ML Tue Jun 22 18:15:44 2010 +0200 @@ -54,6 +54,7 @@ val detailed = ! Output.debugging; fun exn_msg _ (CONTEXT (ctxt, exn)) = exn_msg (SOME ctxt) exn + | exn_msg _ (Exn.EXCEPTIONS []) = "Exception." | exn_msg ctxt (Exn.EXCEPTIONS exns) = cat_lines (map (exn_msg ctxt) exns) | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) = exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc) diff -r 44e42d392c6e -r 9de1add14bac src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Mon Jun 21 19:33:51 2010 +0200 +++ b/src/Pure/PIDE/command.scala Tue Jun 22 18:15:44 2010 +0200 @@ -48,8 +48,7 @@ def name: String = if (is_command) span.head.content else "" override def toString = - if (is_command) name + "(" + id + ")" - else if (is_ignored) "" else "" + id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") /* source text */ diff -r 44e42d392c6e -r 9de1add14bac src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon Jun 21 19:33:51 2010 +0200 +++ b/src/Pure/System/isabelle_system.scala Tue Jun 22 18:15:44 2010 +0200 @@ -12,6 +12,7 @@ BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader, File, IOException} import java.awt.{GraphicsEnvironment, Font} +import java.awt.font.TextAttribute import scala.io.Source import scala.util.matching.Regex @@ -336,31 +337,23 @@ /* fonts */ val font_family = getenv_strict("ISABELLE_FONT_FAMILY") + val font_family_default = "IsabelleText" def get_font(size: Int = 1, bold: Boolean = false): Font = new Font(font_family, if (bold) Font.BOLD else Font.PLAIN, size) + def create_default_font(bold: Boolean = false): Font = + if (bold) + Font.createFont(Font.TRUETYPE_FONT, + platform_file("$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf")) + else + Font.createFont(Font.TRUETYPE_FONT, + platform_file("$ISABELLE_HOME/lib/fonts/IsabelleText.ttf")) + def install_fonts() { - def create_font(bold: Boolean): Font = - { - val name = - if (bold) "$ISABELLE_HOME/lib/fonts/IsabelleTextBold.ttf" - else "$ISABELLE_HOME/lib/fonts/IsabelleText.ttf" - Font.createFont(Font.TRUETYPE_FONT, platform_file(name)) - } - def check_font() = get_font().getFamily == font_family - - if (!check_font()) { - val font = create_font(false) - val bold_font = create_font(true) - - val ge = GraphicsEnvironment.getLocalGraphicsEnvironment() - ge.registerFont(font) - // workaround strange problem with Apple's Java 1.6 font manager - // FIXME does not quite work!? - if (bold_font.getFamily == font_family) ge.registerFont(bold_font) - if (!check_font()) error("Failed to install IsabelleText fonts") - } + val ge = GraphicsEnvironment.getLocalGraphicsEnvironment() + ge.registerFont(create_default_font(bold = false)) + ge.registerFont(create_default_font(bold = true)) } } diff -r 44e42d392c6e -r 9de1add14bac src/Tools/jEdit/src/jedit/isabelle_token_marker.scala --- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Mon Jun 21 19:33:51 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala Tue Jun 22 18:15:44 2010 +0200 @@ -155,9 +155,11 @@ def to: Int => Int = model.to_current(document, _) def from: Int => Int = model.from_current(document, _) + /* FIXME for (text_area <- Isabelle.jedit_text_areas(model.buffer) if Document_View(text_area).isDefined) Document_View(text_area).get.set_styles() + */ def handle_token(style: Byte, offset: Int, length: Int) = handler.handleToken(line_segment, style, offset, length, context) diff -r 44e42d392c6e -r 9de1add14bac src/Tools/jEdit/src/jedit/output_dockable.scala --- a/src/Tools/jEdit/src/jedit/output_dockable.scala Mon Jun 21 19:33:51 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/output_dockable.scala Tue Jun 22 18:15:44 2010 +0200 @@ -129,19 +129,18 @@ reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() } } tracing.selected = show_tracing - tracing.tooltip = - "Indicate output of tracing messages
(also needs to be enabled on the prover side)" + tracing.tooltip = "Indicate output of tracing messages" private val auto_update = new CheckBox("Auto update") { reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() } } auto_update.selected = follow_caret - auto_update.tooltip = "Indicate automatic update following cursor movement" + auto_update.tooltip = "Indicate automatic update following cursor movement" private val update = new Button("Update") { reactions += { case ButtonClicked(_) => handle_caret(); handle_update() } } - update.tooltip = "Update display according to the command at cursor position" + update.tooltip = "Update display according to the command at cursor position" val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, debug, tracing, auto_update, update) add(controls.peer, BorderLayout.NORTH)