1.1 --- a/Admin/isatest/isatest-makedist Wed Jun 15 14:36:41 2011 +0200
1.2 +++ b/Admin/isatest/isatest-makedist Wed Jun 15 15:11:18 2011 +0200
1.3 @@ -98,7 +98,7 @@
1.4
1.5 ## spawn test runs
1.6
1.7 -$SSH macbroy20 "$MAKEALL $HOME/settings/at-poly-test"
1.8 +$SSH macbroy21 "$MAKEALL $HOME/settings/at-poly-test"
1.9 # give test some time to copy settings and start
1.10 sleep 15
1.11 $SSH macbroy28 "$MAKEALL $HOME/settings/at-poly"
2.1 --- a/Admin/isatest/settings/at-poly-test Wed Jun 15 14:36:41 2011 +0200
2.2 +++ b/Admin/isatest/settings/at-poly-test Wed Jun 15 15:11:18 2011 +0200
2.3 @@ -24,7 +24,7 @@
2.4
2.5 ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true"
2.6
2.7 -ISABELLE_GHC="/usr/bin/ghc"
2.8 +ISABELLE_GHC="/home/isabelle/contrib_devel/ghc/x86-linux/ghc"
2.9 ISABELLE_OCAML="/home/isabelle/contrib_devel/ocaml/x86-linux/ocaml"
2.10 ISABELLE_SWIPL="/home/isabelle/contrib_devel/swipl/bin/swipl"
2.11
3.1 --- a/doc-src/IsarRef/Thy/Generic.thy Wed Jun 15 14:36:41 2011 +0200
3.2 +++ b/doc-src/IsarRef/Thy/Generic.thy Wed Jun 15 15:11:18 2011 +0200
3.3 @@ -64,6 +64,8 @@
3.4 @{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\
3.5 @{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\
3.6 @{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\
3.7 + @{method_def intro} & : & @{text method} \\
3.8 + @{method_def elim} & : & @{text method} \\
3.9 @{method_def succeed} & : & @{text method} \\
3.10 @{method_def fail} & : & @{text method} \\
3.11 \end{matharray}
3.12 @@ -73,6 +75,8 @@
3.13 ;
3.14 (@@{method erule} | @@{method drule} | @@{method frule})
3.15 ('(' @{syntax nat} ')')? @{syntax thmrefs}
3.16 + ;
3.17 + (@@{method intro} | @@{method elim}) @{syntax thmrefs}?
3.18 "}
3.19
3.20 \begin{description}
3.21 @@ -103,6 +107,12 @@
3.22 the plain @{method rule} method, with forward chaining of current
3.23 facts.
3.24
3.25 + \item @{method intro} and @{method elim} repeatedly refine some goal
3.26 + by intro- or elim-resolution, after having inserted any chained
3.27 + facts. Exactly the rules given as arguments are taken into account;
3.28 + this allows fine-tuned decomposition of a proof problem, in contrast
3.29 + to common automated tools.
3.30 +
3.31 \item @{method succeed} yields a single (unchanged) result; it is
3.32 the identity of the ``@{text ","}'' method combinator (cf.\
3.33 \secref{sec:proof-meth}).
3.34 @@ -879,6 +889,39 @@
3.35 *}
3.36
3.37
3.38 +subsection {* Structured methods *}
3.39 +
3.40 +text {*
3.41 + \begin{matharray}{rcl}
3.42 + @{method_def rule} & : & @{text method} \\
3.43 + @{method_def contradiction} & : & @{text method} \\
3.44 + \end{matharray}
3.45 +
3.46 + @{rail "
3.47 + @@{method rule} @{syntax thmrefs}?
3.48 + "}
3.49 +
3.50 + \begin{description}
3.51 +
3.52 + \item @{method rule} as offered by the Classical Reasoner is a
3.53 + refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
3.54 + versions work the same, but the classical version observes the
3.55 + classical rule context in addition to that of Isabelle/Pure.
3.56 +
3.57 + Common object logics (HOL, ZF, etc.) declare a rich collection of
3.58 + classical rules (even if these would qualify as intuitionistic
3.59 + ones), but only few declarations to the rule context of
3.60 + Isabelle/Pure (\secref{sec:pure-meth-att}).
3.61 +
3.62 + \item @{method contradiction} solves some goal by contradiction,
3.63 + deriving any result from both @{text "\<not> A"} and @{text A}. Chained
3.64 + facts, which are guaranteed to participate, may appear in either
3.65 + order.
3.66 +
3.67 + \end{description}
3.68 +*}
3.69 +
3.70 +
3.71 subsection {* Automated methods *}
3.72
3.73 text {*
3.74 @@ -892,6 +935,7 @@
3.75 @{method_def fastsimp} & : & @{text method} \\
3.76 @{method_def slowsimp} & : & @{text method} \\
3.77 @{method_def bestsimp} & : & @{text method} \\
3.78 + @{method_def deepen} & : & @{text method} \\
3.79 \end{matharray}
3.80
3.81 @{rail "
3.82 @@ -906,6 +950,8 @@
3.83 (@@{method fastsimp} | @@{method slowsimp} | @@{method bestsimp})
3.84 (@{syntax clasimpmod} * )
3.85 ;
3.86 + @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * )
3.87 + ;
3.88 @{syntax_def clamod}:
3.89 (('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}
3.90 ;
3.91 @@ -990,6 +1036,14 @@
3.92 like @{method fast}, @{method slow}, @{method best}, respectively,
3.93 but use the Simplifier as additional wrapper.
3.94
3.95 + \item @{method deepen} works by exhaustive search up to a certain
3.96 + depth. The start depth is 4 (unless specified explicitly), and the
3.97 + depth is increased iteratively up to 10. Unsafe rules are modified
3.98 + to preserve the formula they act on, so that it be used repeatedly.
3.99 + This method can prove more goals than @{method fast}, but is much
3.100 + slower, for example if the assumptions have many universal
3.101 + quantifiers.
3.102 +
3.103 \end{description}
3.104
3.105 Any of the above methods support additional modifiers of the context
3.106 @@ -1025,13 +1079,8 @@
3.107 \item @{method safe} repeatedly performs safe steps on all subgoals.
3.108 It is deterministic, with at most one outcome.
3.109
3.110 - \item @{method clarify} performs a series of safe steps as follows.
3.111 -
3.112 - No splitting step is applied; for example, the subgoal @{text "A \<and>
3.113 - B"} is left as a conjunction. Proof by assumption, Modus Ponens,
3.114 - etc., may be performed provided they do not instantiate unknowns.
3.115 - Assumptions of the form @{text "x = t"} may be eliminated. The safe
3.116 - wrapper tactical is applied.
3.117 + \item @{method clarify} performs a series of safe steps without
3.118 + splitting subgoals; see also @{ML clarify_step_tac}.
3.119
3.120 \item @{method clarsimp} acts like @{method clarify}, but also does
3.121 simplification. Note that if the Simplifier context includes a
3.122 @@ -1041,42 +1090,47 @@
3.123 *}
3.124
3.125
3.126 -subsection {* Structured proof methods *}
3.127 +subsection {* Single-step tactics *}
3.128
3.129 text {*
3.130 \begin{matharray}{rcl}
3.131 - @{method_def rule} & : & @{text method} \\
3.132 - @{method_def contradiction} & : & @{text method} \\
3.133 - @{method_def intro} & : & @{text method} \\
3.134 - @{method_def elim} & : & @{text method} \\
3.135 + @{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\
3.136 + @{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\
3.137 + @{index_ML step_tac: "Proof.context -> int -> tactic"} \\
3.138 + @{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\
3.139 + @{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\
3.140 \end{matharray}
3.141
3.142 - @{rail "
3.143 - (@@{method rule} | @@{method intro} | @@{method elim}) @{syntax thmrefs}?
3.144 - "}
3.145 + These are the primitive tactics behind the (semi)automated proof
3.146 + methods of the Classical Reasoner. By calling them yourself, you
3.147 + can execute these procedures one step at a time.
3.148
3.149 \begin{description}
3.150
3.151 - \item @{method rule} as offered by the Classical Reasoner is a
3.152 - refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
3.153 - versions work the same, but the classical version observes the
3.154 - classical rule context in addition to that of Isabelle/Pure.
3.155 + \item @{ML safe_step_tac}~@{text "ctxt i"} performs a safe step on
3.156 + subgoal @{text i}. The safe wrapper tacticals are applied to a
3.157 + tactic that may include proof by assumption or Modus Ponens (taking
3.158 + care not to instantiate unknowns), or substitution.
3.159
3.160 - Common object logics (HOL, ZF, etc.) declare a rich collection of
3.161 - classical rules (even if these would qualify as intuitionistic
3.162 - ones), but only few declarations to the rule context of
3.163 - Isabelle/Pure (\secref{sec:pure-meth-att}).
3.164 + \item @{ML inst_step_tac} is like @{ML safe_step_tac}, but allows
3.165 + unknowns to be instantiated.
3.166
3.167 - \item @{method contradiction} solves some goal by contradiction,
3.168 - deriving any result from both @{text "\<not> A"} and @{text A}. Chained
3.169 - facts, which are guaranteed to participate, may appear in either
3.170 - order.
3.171 + \item @{ML step_tac}~@{text "ctxt i"} is the basic step of the proof
3.172 + procedure. The unsafe wrapper tacticals are applied to a tactic
3.173 + that tries @{ML safe_tac}, @{ML inst_step_tac}, or applies an unsafe
3.174 + rule from the context.
3.175
3.176 - \item @{method intro} and @{method elim} repeatedly refine some goal
3.177 - by intro- or elim-resolution, after having inserted any chained
3.178 - facts. Exactly the rules given as arguments are taken into account;
3.179 - this allows fine-tuned decomposition of a proof problem, in contrast
3.180 - to common automated tools.
3.181 + \item @{ML slow_step_tac} resembles @{ML step_tac}, but allows
3.182 + backtracking between using safe rules with instantiation (@{ML
3.183 + inst_step_tac}) and using unsafe rules. The resulting search space
3.184 + is larger.
3.185 +
3.186 + \item @{ML clarify_step_tac}~@{text "ctxt i"} performs a safe step
3.187 + on subgoal @{text i}. No splitting step is applied; for example,
3.188 + the subgoal @{text "A \<and> B"} is left as a conjunction. Proof by
3.189 + assumption, Modus Ponens, etc., may be performed provided they do
3.190 + not instantiate unknowns. Assumptions of the form @{text "x = t"}
3.191 + may be eliminated. The safe wrapper tactical is applied.
3.192
3.193 \end{description}
3.194 *}
4.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex Wed Jun 15 14:36:41 2011 +0200
4.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex Wed Jun 15 15:11:18 2011 +0200
4.3 @@ -123,6 +123,8 @@
4.4 \indexdef{}{method}{erule}\hypertarget{method.erule}{\hyperlink{method.erule}{\mbox{\isa{erule}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
4.5 \indexdef{}{method}{drule}\hypertarget{method.drule}{\hyperlink{method.drule}{\mbox{\isa{drule}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
4.6 \indexdef{}{method}{frule}\hypertarget{method.frule}{\hyperlink{method.frule}{\mbox{\isa{frule}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{method} \\
4.7 + \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
4.8 + \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
4.9 \indexdef{}{method}{succeed}\hypertarget{method.succeed}{\hyperlink{method.succeed}{\mbox{\isa{succeed}}}} & : & \isa{method} \\
4.10 \indexdef{}{method}{fail}\hypertarget{method.fail}{\hyperlink{method.fail}{\mbox{\isa{fail}}}} & : & \isa{method} \\
4.11 \end{matharray}
4.12 @@ -154,6 +156,17 @@
4.13 \rail@endbar
4.14 \rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
4.15 \rail@end
4.16 +\rail@begin{2}{}
4.17 +\rail@bar
4.18 +\rail@term{\hyperlink{method.intro}{\mbox{\isa{intro}}}}[]
4.19 +\rail@nextbar{1}
4.20 +\rail@term{\hyperlink{method.elim}{\mbox{\isa{elim}}}}[]
4.21 +\rail@endbar
4.22 +\rail@bar
4.23 +\rail@nextbar{1}
4.24 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
4.25 +\rail@endbar
4.26 +\rail@end
4.27 \end{railoutput}
4.28
4.29
4.30 @@ -182,6 +195,12 @@
4.31 the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method, with forward chaining of current
4.32 facts.
4.33
4.34 + \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
4.35 + by intro- or elim-resolution, after having inserted any chained
4.36 + facts. Exactly the rules given as arguments are taken into account;
4.37 + this allows fine-tuned decomposition of a proof problem, in contrast
4.38 + to common automated tools.
4.39 +
4.40 \item \hyperlink{method.succeed}{\mbox{\isa{succeed}}} yields a single (unchanged) result; it is
4.41 the identity of the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}}'' method combinator (cf.\
4.42 \secref{sec:proof-meth}).
4.43 @@ -1311,6 +1330,48 @@
4.44 \end{isamarkuptext}%
4.45 \isamarkuptrue%
4.46 %
4.47 +\isamarkupsubsection{Structured methods%
4.48 +}
4.49 +\isamarkuptrue%
4.50 +%
4.51 +\begin{isamarkuptext}%
4.52 +\begin{matharray}{rcl}
4.53 + \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
4.54 + \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
4.55 + \end{matharray}
4.56 +
4.57 + \begin{railoutput}
4.58 +\rail@begin{2}{}
4.59 +\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
4.60 +\rail@bar
4.61 +\rail@nextbar{1}
4.62 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
4.63 +\rail@endbar
4.64 +\rail@end
4.65 +\end{railoutput}
4.66 +
4.67 +
4.68 + \begin{description}
4.69 +
4.70 + \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
4.71 + refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
4.72 + versions work the same, but the classical version observes the
4.73 + classical rule context in addition to that of Isabelle/Pure.
4.74 +
4.75 + Common object logics (HOL, ZF, etc.) declare a rich collection of
4.76 + classical rules (even if these would qualify as intuitionistic
4.77 + ones), but only few declarations to the rule context of
4.78 + Isabelle/Pure (\secref{sec:pure-meth-att}).
4.79 +
4.80 + \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
4.81 + deriving any result from both \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequote}}} and \isa{A}. Chained
4.82 + facts, which are guaranteed to participate, may appear in either
4.83 + order.
4.84 +
4.85 + \end{description}%
4.86 +\end{isamarkuptext}%
4.87 +\isamarkuptrue%
4.88 +%
4.89 \isamarkupsubsection{Automated methods%
4.90 }
4.91 \isamarkuptrue%
4.92 @@ -1326,6 +1387,7 @@
4.93 \indexdef{}{method}{fastsimp}\hypertarget{method.fastsimp}{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}} & : & \isa{method} \\
4.94 \indexdef{}{method}{slowsimp}\hypertarget{method.slowsimp}{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}} & : & \isa{method} \\
4.95 \indexdef{}{method}{bestsimp}\hypertarget{method.bestsimp}{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}} & : & \isa{method} \\
4.96 + \indexdef{}{method}{deepen}\hypertarget{method.deepen}{\hyperlink{method.deepen}{\mbox{\isa{deepen}}}} & : & \isa{method} \\
4.97 \end{matharray}
4.98
4.99 \begin{railoutput}
4.100 @@ -1385,6 +1447,17 @@
4.101 \rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
4.102 \rail@endplus
4.103 \rail@end
4.104 +\rail@begin{2}{}
4.105 +\rail@term{\hyperlink{method.deepen}{\mbox{\isa{deepen}}}}[]
4.106 +\rail@bar
4.107 +\rail@nextbar{1}
4.108 +\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
4.109 +\rail@endbar
4.110 +\rail@plus
4.111 +\rail@nextplus{1}
4.112 +\rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
4.113 +\rail@endplus
4.114 +\rail@end
4.115 \rail@begin{4}{\indexdef{}{syntax}{clamod}\hypertarget{syntax.clamod}{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}}
4.116 \rail@bar
4.117 \rail@bar
4.118 @@ -1541,6 +1614,14 @@
4.119 like \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, respectively,
4.120 but use the Simplifier as additional wrapper.
4.121
4.122 + \item \hyperlink{method.deepen}{\mbox{\isa{deepen}}} works by exhaustive search up to a certain
4.123 + depth. The start depth is 4 (unless specified explicitly), and the
4.124 + depth is increased iteratively up to 10. Unsafe rules are modified
4.125 + to preserve the formula they act on, so that it be used repeatedly.
4.126 + This method can prove more goals than \hyperlink{method.fast}{\mbox{\isa{fast}}}, but is much
4.127 + slower, for example if the assumptions have many universal
4.128 + quantifiers.
4.129 +
4.130 \end{description}
4.131
4.132 Any of the above methods support additional modifiers of the context
4.133 @@ -1595,12 +1676,8 @@
4.134 \item \hyperlink{method.safe}{\mbox{\isa{safe}}} repeatedly performs safe steps on all subgoals.
4.135 It is deterministic, with at most one outcome.
4.136
4.137 - \item \hyperlink{method.clarify}{\mbox{\isa{clarify}}} performs a series of safe steps as follows.
4.138 -
4.139 - No splitting step is applied; for example, the subgoal \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequote}}} is left as a conjunction. Proof by assumption, Modus Ponens,
4.140 - etc., may be performed provided they do not instantiate unknowns.
4.141 - Assumptions of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} may be eliminated. The safe
4.142 - wrapper tactical is applied.
4.143 + \item \hyperlink{method.clarify}{\mbox{\isa{clarify}}} performs a series of safe steps without
4.144 + splitting subgoals; see also \verb|clarify_step_tac|.
4.145
4.146 \item \hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}} acts like \hyperlink{method.clarify}{\mbox{\isa{clarify}}}, but also does
4.147 simplification. Note that if the Simplifier context includes a
4.148 @@ -1610,57 +1687,48 @@
4.149 \end{isamarkuptext}%
4.150 \isamarkuptrue%
4.151 %
4.152 -\isamarkupsubsection{Structured proof methods%
4.153 +\isamarkupsubsection{Single-step tactics%
4.154 }
4.155 \isamarkuptrue%
4.156 %
4.157 \begin{isamarkuptext}%
4.158 \begin{matharray}{rcl}
4.159 - \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
4.160 - \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
4.161 - \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
4.162 - \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
4.163 + \indexdef{}{ML}{safe\_step\_tac}\verb|safe_step_tac: Proof.context -> int -> tactic| \\
4.164 + \indexdef{}{ML}{inst\_step\_tac}\verb|inst_step_tac: Proof.context -> int -> tactic| \\
4.165 + \indexdef{}{ML}{step\_tac}\verb|step_tac: Proof.context -> int -> tactic| \\
4.166 + \indexdef{}{ML}{slow\_step\_tac}\verb|slow_step_tac: Proof.context -> int -> tactic| \\
4.167 + \indexdef{}{ML}{clarify\_step\_tac}\verb|clarify_step_tac: Proof.context -> int -> tactic| \\
4.168 \end{matharray}
4.169
4.170 - \begin{railoutput}
4.171 -\rail@begin{3}{}
4.172 -\rail@bar
4.173 -\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
4.174 -\rail@nextbar{1}
4.175 -\rail@term{\hyperlink{method.intro}{\mbox{\isa{intro}}}}[]
4.176 -\rail@nextbar{2}
4.177 -\rail@term{\hyperlink{method.elim}{\mbox{\isa{elim}}}}[]
4.178 -\rail@endbar
4.179 -\rail@bar
4.180 -\rail@nextbar{1}
4.181 -\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
4.182 -\rail@endbar
4.183 -\rail@end
4.184 -\end{railoutput}
4.185 -
4.186 + These are the primitive tactics behind the (semi)automated proof
4.187 + methods of the Classical Reasoner. By calling them yourself, you
4.188 + can execute these procedures one step at a time.
4.189
4.190 \begin{description}
4.191
4.192 - \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
4.193 - refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
4.194 - versions work the same, but the classical version observes the
4.195 - classical rule context in addition to that of Isabelle/Pure.
4.196 + \item \verb|safe_step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} performs a safe step on
4.197 + subgoal \isa{i}. The safe wrapper tacticals are applied to a
4.198 + tactic that may include proof by assumption or Modus Ponens (taking
4.199 + care not to instantiate unknowns), or substitution.
4.200
4.201 - Common object logics (HOL, ZF, etc.) declare a rich collection of
4.202 - classical rules (even if these would qualify as intuitionistic
4.203 - ones), but only few declarations to the rule context of
4.204 - Isabelle/Pure (\secref{sec:pure-meth-att}).
4.205 + \item \verb|inst_step_tac| is like \verb|safe_step_tac|, but allows
4.206 + unknowns to be instantiated.
4.207
4.208 - \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
4.209 - deriving any result from both \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequote}}} and \isa{A}. Chained
4.210 - facts, which are guaranteed to participate, may appear in either
4.211 - order.
4.212 + \item \verb|step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} is the basic step of the proof
4.213 + procedure. The unsafe wrapper tacticals are applied to a tactic
4.214 + that tries \verb|safe_tac|, \verb|inst_step_tac|, or applies an unsafe
4.215 + rule from the context.
4.216
4.217 - \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
4.218 - by intro- or elim-resolution, after having inserted any chained
4.219 - facts. Exactly the rules given as arguments are taken into account;
4.220 - this allows fine-tuned decomposition of a proof problem, in contrast
4.221 - to common automated tools.
4.222 + \item \verb|slow_step_tac| resembles \verb|step_tac|, but allows
4.223 + backtracking between using safe rules with instantiation (\verb|inst_step_tac|) and using unsafe rules. The resulting search space
4.224 + is larger.
4.225 +
4.226 + \item \verb|clarify_step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} performs a safe step
4.227 + on subgoal \isa{i}. No splitting step is applied; for example,
4.228 + the subgoal \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequote}}} is left as a conjunction. Proof by
4.229 + assumption, Modus Ponens, etc., may be performed provided they do
4.230 + not instantiate unknowns. Assumptions of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}}
4.231 + may be eliminated. The safe wrapper tactical is applied.
4.232
4.233 \end{description}%
4.234 \end{isamarkuptext}%
5.1 --- a/doc-src/Ref/classical.tex Wed Jun 15 14:36:41 2011 +0200
5.2 +++ b/doc-src/Ref/classical.tex Wed Jun 15 15:11:18 2011 +0200
5.3 @@ -125,21 +125,6 @@
5.4
5.5 \section{The classical tactics}
5.6
5.7 -\subsection{Semi-automatic tactics}
5.8 -\begin{ttbox}
5.9 -clarify_step_tac : claset -> int -> tactic
5.10 -\end{ttbox}
5.11 -
5.12 -\begin{ttdescription}
5.13 -\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
5.14 - subgoal~$i$. No splitting step is applied; for example, the subgoal $A\conj
5.15 - B$ is left as a conjunction. Proof by assumption, Modus Ponens, etc., may be
5.16 - performed provided they do not instantiate unknowns. Assumptions of the
5.17 - form $x=t$ may be eliminated. The user-supplied safe wrapper tactical is
5.18 - applied.
5.19 -\end{ttdescription}
5.20 -
5.21 -
5.22 \subsection{Other classical tactics}
5.23 \begin{ttbox}
5.24 slow_best_tac : claset -> int -> tactic
5.25 @@ -151,58 +136,6 @@
5.26 \end{ttdescription}
5.27
5.28
5.29 -\subsection{Depth-limited automatic tactics}
5.30 -\begin{ttbox}
5.31 -depth_tac : claset -> int -> int -> tactic
5.32 -deepen_tac : claset -> int -> int -> tactic
5.33 -\end{ttbox}
5.34 -These work by exhaustive search up to a specified depth. Unsafe rules are
5.35 -modified to preserve the formula they act on, so that it be used repeatedly.
5.36 -They can prove more goals than \texttt{fast_tac} can but are much
5.37 -slower, for example if the assumptions have many universal quantifiers.
5.38 -
5.39 -The depth limits the number of unsafe steps. If you can estimate the minimum
5.40 -number of unsafe steps needed, supply this value as~$m$ to save time.
5.41 -\begin{ttdescription}
5.42 -\item[\ttindexbold{depth_tac} $cs$ $m$ $i$]
5.43 -tries to prove subgoal~$i$ by exhaustive search up to depth~$m$.
5.44 -
5.45 -\item[\ttindexbold{deepen_tac} $cs$ $m$ $i$]
5.46 -tries to prove subgoal~$i$ by iterative deepening. It calls \texttt{depth_tac}
5.47 -repeatedly with increasing depths, starting with~$m$.
5.48 -\end{ttdescription}
5.49 -
5.50 -
5.51 -\subsection{Single-step tactics}
5.52 -\begin{ttbox}
5.53 -safe_step_tac : claset -> int -> tactic
5.54 -inst_step_tac : claset -> int -> tactic
5.55 -step_tac : claset -> int -> tactic
5.56 -slow_step_tac : claset -> int -> tactic
5.57 -\end{ttbox}
5.58 -The automatic proof procedures call these tactics. By calling them
5.59 -yourself, you can execute these procedures one step at a time.
5.60 -\begin{ttdescription}
5.61 -\item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
5.62 - subgoal~$i$. The safe wrapper tacticals are applied to a tactic that may
5.63 - include proof by assumption or Modus Ponens (taking care not to instantiate
5.64 - unknowns), or substitution.
5.65 -
5.66 -\item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac},
5.67 -but allows unknowns to be instantiated.
5.68 -
5.69 -\item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof
5.70 - procedure. The unsafe wrapper tacticals are applied to a tactic that tries
5.71 - \texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule
5.72 - from~$cs$.
5.73 -
5.74 -\item[\ttindexbold{slow_step_tac}]
5.75 - resembles \texttt{step_tac}, but allows backtracking between using safe
5.76 - rules with instantiation (\texttt{inst_step_tac}) and using unsafe rules.
5.77 - The resulting search space is larger.
5.78 -\end{ttdescription}
5.79 -
5.80 -
5.81 \subsection{Other useful tactics}
5.82 \index{tactics!for contradiction}
5.83 \index{tactics!for Modus Ponens}
6.1 --- a/src/HOL/Library/Executable_Set.thy Wed Jun 15 14:36:41 2011 +0200
6.2 +++ b/src/HOL/Library/Executable_Set.thy Wed Jun 15 15:11:18 2011 +0200
6.3 @@ -12,7 +12,7 @@
6.4 text {*
6.5 This is just an ad-hoc hack which will rarely give you what you want.
6.6 For the moment, whenever you need executable sets, consider using
6.7 - type @{text fset} from theory @{text Cset}.
6.8 + type @{text Cset.set} from theory @{text Cset}.
6.9 *}
6.10
6.11 declare mem_def [code del]
7.1 --- a/src/HOL/Mutabelle/lib/Tools/mutabelle Wed Jun 15 14:36:41 2011 +0200
7.2 +++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Wed Jun 15 15:11:18 2011 +0200
7.3 @@ -90,7 +90,7 @@
7.4 MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\" #> Config.put Quickcheck.finite_types false) \"exhaustive_nft\",
7.5 MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"narrowing\" #> Config.put Quickcheck.finite_types false) \"narrowing\",
7.6 MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"narrowing\" #> Config.put Quickcheck.finite_types false
7.7 - #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ int}])))) \"narrowing_nat\"
7.8 + #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\"
7.9 (* MutabelleExtra.nitpick_mtd *)
7.10 ]
7.11 *}
8.1 --- a/src/HOL/Quickcheck_Narrowing.thy Wed Jun 15 14:36:41 2011 +0200
8.2 +++ b/src/HOL/Quickcheck_Narrowing.thy Wed Jun 15 15:11:18 2011 +0200
8.3 @@ -207,14 +207,6 @@
8.4 subsubsection {* Narrowing's deep representation of types and terms *}
8.5
8.6 datatype narrowing_type = SumOfProd "narrowing_type list list"
8.7 -text {*
8.8 -The definition of the automatically derived equal type class instance for @{typ narrowing_type}
8.9 -causes an error in the OCaml serializer.
8.10 -For the moment, we delete this equation manually because we do not require an executable equality
8.11 -on this type anyway.
8.12 -*}
8.13 -declare Quickcheck_Narrowing.equal_narrowing_type_def[code del]
8.14 -
8.15 datatype narrowing_term = Var "code_int list" narrowing_type | Ctr code_int "narrowing_term list"
8.16 datatype 'a cons = C narrowing_type "(narrowing_term list => 'a) list"
8.17
9.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Jun 15 14:36:41 2011 +0200
9.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Jun 15 15:11:18 2011 +0200
9.3 @@ -209,6 +209,10 @@
9.4 val path = Path.append (Path.explode "~/.isabelle") (Path.basic (name ^ serial_string ()))
9.5 val _ = Isabelle_System.mkdirs path;
9.6 in Exn.release (Exn.capture f path) end;
9.7 +
9.8 +fun elapsed_time description e =
9.9 + let val ({elapsed, ...}, result) = Timing.timing e ()
9.10 + in (result, (description, Time.toMilliseconds elapsed)) end
9.11
9.12 fun value (contains_existentials, (quiet, size)) ctxt (get, put, put_ml) (code, value_name) =
9.13 let
9.14 @@ -237,20 +241,23 @@
9.15 val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
9.16 (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
9.17 " -o " ^ executable ^ ";"
9.18 + val (result, compilation_time) = elapsed_time "Haskell compilation" (fn () => bash cmd)
9.19 val _ = if bash cmd <> 0 then error "Compilation with GHC failed" else ()
9.20 - fun with_size k =
9.21 + fun with_size k exec_times =
9.22 if k > size then
9.23 - NONE
9.24 + (NONE, exec_times)
9.25 else
9.26 let
9.27 val _ = message ("Test data size: " ^ string_of_int k)
9.28 - val (response, _) = bash_output (executable ^ " " ^ string_of_int k)
9.29 + val ((response, _), exec_time) = elapsed_time ("execution of size " ^ string_of_int k)
9.30 + (fn () => bash_output (executable ^ " " ^ string_of_int k))
9.31 in
9.32 - if response = "NONE\n" then with_size (k + 1) else SOME response
9.33 + if response = "NONE\n" then with_size (k + 1) (exec_time :: exec_times)
9.34 + else (SOME response, exec_time :: exec_times)
9.35 end
9.36 - in case with_size 0 of
9.37 - NONE => NONE
9.38 - | SOME response =>
9.39 + in case with_size 0 [compilation_time] of
9.40 + (NONE, exec_times) => (NONE, exec_times)
9.41 + | (SOME response, exec_times) =>
9.42 let
9.43 val output_value = the_default "NONE"
9.44 (try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
9.45 @@ -260,7 +267,7 @@
9.46 val ctxt' = ctxt
9.47 |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
9.48 |> Context.proof_map (exec false ml_code);
9.49 - in get ctxt' () end
9.50 + in (get ctxt' (), exec_times) end
9.51 end
9.52 in with_tmp_dir tmp_prefix run end;
9.53
9.54 @@ -389,14 +396,14 @@
9.55 val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
9.56 ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
9.57 val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt')
9.58 - val result = dynamic_value_strict (true, opts)
9.59 + val (result, timings) = dynamic_value_strict (true, opts)
9.60 (Existential_Counterexample.get, Existential_Counterexample.put,
9.61 "Narrowing_Generators.put_existential_counterexample")
9.62 - thy' (Option.map o map_counterexample) (mk_property qs prop_def')
9.63 + thy' (apfst o Option.map o map_counterexample) (mk_property qs prop_def')
9.64 val result' = Option.map (mk_terms ctxt' (fst (strip_quantifiers pnf_t))) result
9.65 in
9.66 Quickcheck.Result {counterexample = result', evaluation_terms = Option.map (K []) result,
9.67 - timings = [], reports = []}
9.68 + timings = timings, reports = []}
9.69 end
9.70 else
9.71 let
9.72 @@ -405,12 +412,12 @@
9.73 val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
9.74 fun ensure_testable t =
9.75 Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
9.76 - val result = dynamic_value_strict (false, opts)
9.77 + val (result, timings) = dynamic_value_strict (false, opts)
9.78 (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
9.79 - thy (Option.map o map) (ensure_testable (finitize t'))
9.80 + thy (apfst o Option.map o map) (ensure_testable (finitize t'))
9.81 in
9.82 Quickcheck.Result {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) result,
9.83 - evaluation_terms = Option.map (K []) result, timings = [], reports = []}
9.84 + evaluation_terms = Option.map (K []) result, timings = timings, reports = []}
9.85 end
9.86 end;
9.87
10.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML Wed Jun 15 14:36:41 2011 +0200
10.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML Wed Jun 15 15:11:18 2011 +0200
10.3 @@ -32,12 +32,11 @@
10.4 val vars = the (get_first get_vars descr) ~~ Ts
10.5 val lookup_var = the o AList.lookup (op =) vars
10.6
10.7 - val dTs = map (apsnd (fn (m, vs, _) => Type (m, map lookup_var vs))) descr
10.8 - val lookup_typ = the o AList.lookup (op =) dTs
10.9 -
10.10 fun typ_of (dt as Datatype.DtTFree _) = lookup_var dt
10.11 - | typ_of (Datatype.DtType (n, dts)) = Type (n, map typ_of dts)
10.12 - | typ_of (Datatype.DtRec i) = lookup_typ i
10.13 + | typ_of (Datatype.DtType (m, dts)) = Type (m, map typ_of dts)
10.14 + | typ_of (Datatype.DtRec i) =
10.15 + the (AList.lookup (op =) descr i)
10.16 + |> (fn (m, dts, _) => Type (m, map typ_of dts))
10.17
10.18 fun mk_constr T (m, dts) ctxt =
10.19 let
10.20 @@ -48,7 +47,7 @@
10.21
10.22 fun mk_decl (i, (_, _, constrs)) ctxt =
10.23 let
10.24 - val T = lookup_typ i
10.25 + val T = typ_of (Datatype.DtRec i)
10.26 val (css, ctxt') = fold_map (mk_constr T) constrs ctxt
10.27 in ((T, css), ctxt') end
10.28
10.29 @@ -87,6 +86,7 @@
10.30 (* collection of declarations *)
10.31
10.32 fun declared declss T = exists (exists (equal T o fst)) declss
10.33 +fun declared' dss T = exists (exists (equal T o fst) o snd) dss
10.34
10.35 fun get_decls T n Ts ctxt =
10.36 let val thy = Proof_Context.theory_of ctxt
10.37 @@ -104,13 +104,15 @@
10.38
10.39 fun add_decls T (declss, ctxt) =
10.40 let
10.41 + fun depends Ts ds = exists (member (op =) (map fst ds)) Ts
10.42 +
10.43 fun add (TFree _) = I
10.44 | add (TVar _) = I
10.45 | add (T as Type (@{type_name fun}, _)) =
10.46 fold add (Term.body_type T :: Term.binder_types T)
10.47 | add @{typ bool} = I
10.48 | add (T as Type (n, Ts)) = (fn (dss, ctxt1) =>
10.49 - if declared declss T orelse declared dss T then (dss, ctxt1)
10.50 + if declared declss T orelse declared' dss T then (dss, ctxt1)
10.51 else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1)
10.52 else
10.53 (case get_decls T n Ts ctxt1 of
10.54 @@ -120,7 +122,13 @@
10.55 val constrTs =
10.56 maps (map (snd o Term.dest_Const o fst) o snd) ds
10.57 val Us = fold (union (op =) o Term.binder_types) constrTs []
10.58 - in fold add Us (ds :: dss, ctxt2) end))
10.59 - in add T ([], ctxt) |>> append declss end
10.60 +
10.61 + fun ins [] = [(Us, ds)]
10.62 + | ins ((Uds as (Us', _)) :: Udss) =
10.63 + if depends Us' ds then (Us, ds) :: Uds :: Udss
10.64 + else Uds :: ins Udss
10.65 + in fold add Us (ins dss, ctxt2) end))
10.66 + in add T ([], ctxt) |>> append declss o map snd end
10.67 +
10.68
10.69 end
11.1 --- a/src/HOL/Tools/SMT/smt_translate.ML Wed Jun 15 14:36:41 2011 +0200
11.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Jun 15 15:11:18 2011 +0200
11.3 @@ -160,7 +160,6 @@
11.4 Termtab.update (constr, length selects) #>
11.5 fold (Termtab.update o rpair 1) selects
11.6 val funcs = fold (fold (fold add o snd)) declss Termtab.empty
11.7 -
11.8 in ((funcs, declss', tr_context', ctxt'), ts) end
11.9 (* FIXME: also return necessary datatype and record theorems *)
11.10
11.11 @@ -344,11 +343,14 @@
11.12 in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end
11.13 in
11.14
11.15 -fun intro_explicit_application ctxt ts =
11.16 +fun intro_explicit_application ctxt funcs ts =
11.17 let
11.18 val (arities, types) = fold min_arities ts (Termtab.empty, Typtab.empty)
11.19 val arities' = Termtab.map (minimize types) arities
11.20 - fun apply' t = apply (the (Termtab.lookup arities' t)) t
11.21 +
11.22 + fun app_func t T ts =
11.23 + if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts)
11.24 + else apply (the (Termtab.lookup arities' t)) t T ts
11.25
11.26 fun traverse Ts t =
11.27 (case Term.strip_comb t of
11.28 @@ -359,8 +361,8 @@
11.29 | (u as Const (c as (_, T)), ts) =>
11.30 (case SMT_Builtin.dest_builtin ctxt c ts of
11.31 SOME (_, _, us, mk) => mk (map (traverse Ts) us)
11.32 - | NONE => apply' u T (map (traverse Ts) ts))
11.33 - | (u as Free (_, T), ts) => apply' u T (map (traverse Ts) ts)
11.34 + | NONE => app_func u T (map (traverse Ts) ts))
11.35 + | (u as Free (_, T), ts) => app_func u T (map (traverse Ts) ts)
11.36 | (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)
11.37 | (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts
11.38 | (u, ts) => traverses Ts u ts)
11.39 @@ -586,7 +588,7 @@
11.40 ts2
11.41 |> eta_expand ctxt1 is_fol funcs
11.42 |> lift_lambdas ctxt1
11.43 - |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1)
11.44 + |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs)
11.45
11.46 val ((rewrite_rules, extra_thms, builtin), ts4) =
11.47 (if is_fol then folify ctxt2 else pair ([], [], I)) ts3
12.1 --- a/src/Pure/General/markup.scala Wed Jun 15 14:36:41 2011 +0200
12.2 +++ b/src/Pure/General/markup.scala Wed Jun 15 15:11:18 2011 +0200
12.3 @@ -167,6 +167,7 @@
12.4 val XNUM = "xnum"
12.5 val XSTR = "xstr"
12.6 val LITERAL = "literal"
12.7 + val INNER_STRING = "inner_string"
12.8 val INNER_COMMENT = "inner_comment"
12.9
12.10 val TOKEN_RANGE = "token_range"
13.1 --- a/src/Tools/jEdit/lib/Tools/jedit Wed Jun 15 14:36:41 2011 +0200
13.2 +++ b/src/Tools/jEdit/lib/Tools/jedit Wed Jun 15 15:11:18 2011 +0200
13.3 @@ -23,6 +23,7 @@
13.4 "src/raw_output_dockable.scala"
13.5 "src/scala_console.scala"
13.6 "src/session_dockable.scala"
13.7 + "src/text_area_painter.scala"
13.8 )
13.9
13.10 declare -a RESOURCES=(
13.11 @@ -165,15 +166,29 @@
13.12
13.13 TARGET="dist/jars/Isabelle-jEdit.jar"
13.14
13.15 +declare -a UPDATED=()
13.16 +
13.17 if [ "$BUILD_JARS" = jars_fresh ]; then
13.18 OUTDATED=true
13.19 else
13.20 OUTDATED=false
13.21 - for SOURCE in "${SOURCES[@]}" "${RESOURCES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}"
13.22 - do
13.23 - [ ! -e "$SOURCE" ] && fail "Missing file: $SOURCE"
13.24 - [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true
13.25 - done
13.26 + if [ ! -e "$TARGET" ]; then
13.27 + OUTDATED=true
13.28 + else
13.29 + if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
13.30 + declare -a DEPS=("${SOURCES[@]}" "${RESOURCES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}")
13.31 + else
13.32 + declare -a DEPS=("${SOURCES[@]}" "${RESOURCES[@]}")
13.33 + fi
13.34 + for DEP in "${DEPS[@]}"
13.35 + do
13.36 + [ ! -e "$DEP" ] && fail "Missing file: $DEP"
13.37 + [ "$DEP" -nt "$TARGET" ] && {
13.38 + OUTDATED=true
13.39 + UPDATED["${#UPDATED[@]}"]="$DEP"
13.40 + }
13.41 + done
13.42 + fi
13.43 fi
13.44
13.45
13.46 @@ -181,6 +196,14 @@
13.47
13.48 if [ "$OUTDATED" = true ]
13.49 then
13.50 + [ "${#UPDATED[@]}" -gt 0 ] && {
13.51 + echo "Rebuild due to updated file dependencies:"
13.52 + for FILE in "${UPDATED[@]}"
13.53 + do
13.54 + echo " $FILE"
13.55 + done
13.56 + }
13.57 +
13.58 [ -z "$SCALA_HOME" ] && fail "Unknown SCALA_HOME -- Scala unavailable"
13.59
13.60 [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/Tools/jEdit/patches/scriptstyles Wed Jun 15 15:11:18 2011 +0200
14.3 @@ -0,0 +1,30 @@
14.4 +diff -r jEdit/org/gjt/sp/jedit/syntax/Token.java jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
14.5 +60c60
14.6 +< return (token == Token.END) ? "END" : TOKEN_TYPES[token];
14.7 +---
14.8 +> return (token == Token.END) ? "END" : TOKEN_TYPES[(token >= ID_COUNT) ? 0 : token];
14.9 +diff -r jEdit/org/gjt/sp/util/SyntaxUtilities.java jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
14.10 +196a197,207
14.11 +> * Style with sub/superscript font attribute.
14.12 +> */
14.13 +> public static SyntaxStyle scriptStyle(String family, int size, int script)
14.14 +> {
14.15 +> Font font = new Font(family, 0, size);
14.16 +> java.util.Map attributes = new java.util.HashMap();
14.17 +> attributes.put(java.awt.font.TextAttribute.SUPERSCRIPT, new Integer(script));
14.18 +> return new SyntaxStyle(Color.black, null, font.deriveFont(attributes));
14.19 +> }
14.20 +>
14.21 +> /**
14.22 +206c217
14.23 +< SyntaxStyle[] styles = new SyntaxStyle[Token.ID_COUNT];
14.24 +---
14.25 +> SyntaxStyle[] styles = new SyntaxStyle[Token.ID_COUNT + 2];
14.26 +209c220
14.27 +< for(int i = 1; i < styles.length; i++)
14.28 +---
14.29 +> for(int i = 1; i < Token.ID_COUNT; i++)
14.30 +225a237,239
14.31 +> styles[Token.ID_COUNT] = scriptStyle(family, size, -1);
14.32 +> styles[Token.ID_COUNT + 1] = scriptStyle(family, size, 1);
14.33 +>
15.1 --- a/src/Tools/jEdit/src/document_model.scala Wed Jun 15 14:36:41 2011 +0200
15.2 +++ b/src/Tools/jEdit/src/document_model.scala Wed Jun 15 15:11:18 2011 +0200
15.3 @@ -25,36 +25,6 @@
15.4 {
15.5 object Token_Markup
15.6 {
15.7 - /* extended token styles */
15.8 -
15.9 - private val plain_range: Int = Token.ID_COUNT
15.10 - private val full_range: Int = 3 * plain_range
15.11 - private def check_range(i: Int) { require(0 <= i && i < plain_range) }
15.12 -
15.13 - def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
15.14 - def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
15.15 -
15.16 - private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
15.17 - {
15.18 - import scala.collection.JavaConversions._
15.19 - val script_font =
15.20 - style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
15.21 - new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font)
15.22 - }
15.23 -
15.24 - def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
15.25 - {
15.26 - val new_styles = new Array[SyntaxStyle](full_range)
15.27 - for (i <- 0 until plain_range) {
15.28 - val style = styles(i)
15.29 - new_styles(i) = style
15.30 - new_styles(subscript(i.toByte)) = script_style(style, -1)
15.31 - new_styles(superscript(i.toByte)) = script_style(style, 1)
15.32 - }
15.33 - new_styles
15.34 - }
15.35 -
15.36 -
15.37 /* line context */
15.38
15.39 private val dummy_rules = new ParserRuleSet("isabelle", "MAIN")
15.40 @@ -197,12 +167,6 @@
15.41 val start = buffer.getLineStartOffset(line)
15.42 val stop = start + line_segment.count
15.43
15.44 - /* FIXME
15.45 - for (text_area <- Isabelle.jedit_text_areas(buffer)
15.46 - if Document_View(text_area).isDefined)
15.47 - Document_View(text_area).get.set_styles()
15.48 - */
15.49 -
15.50 def handle_token(style: Byte, offset: Text.Offset, length: Int) =
15.51 handler.handleToken(line_segment, style, offset, length, context)
15.52
16.1 --- a/src/Tools/jEdit/src/document_view.scala Wed Jun 15 14:36:41 2011 +0200
16.2 +++ b/src/Tools/jEdit/src/document_view.scala Wed Jun 15 15:11:18 2011 +0200
16.3 @@ -17,13 +17,12 @@
16.4 FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
16.5 import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
16.6 import javax.swing.event.{CaretListener, CaretEvent}
16.7 -import java.util.ArrayList
16.8
16.9 import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
16.10 import org.gjt.sp.jedit.gui.RolloverButton
16.11 import org.gjt.sp.jedit.options.GutterOptionPane
16.12 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
16.13 -import org.gjt.sp.jedit.syntax.{SyntaxStyle, DisplayTokenHandler, Chunk, Token}
16.14 +import org.gjt.sp.jedit.syntax.{SyntaxStyle}
16.15
16.16
16.17 object Document_View
16.18 @@ -63,77 +62,13 @@
16.19 }
16.20
16.21
16.22 -class Document_View(val model: Document_Model, text_area: JEditTextArea)
16.23 +class Document_View(val model: Document_Model, val text_area: JEditTextArea)
16.24 {
16.25 private val session = model.session
16.26
16.27
16.28 /** token handling **/
16.29
16.30 - /* extended token styles */
16.31 -
16.32 - private var styles: Array[SyntaxStyle] = null // owned by Swing thread
16.33 -
16.34 - def extend_styles()
16.35 - {
16.36 - Swing_Thread.require()
16.37 - styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
16.38 - }
16.39 - extend_styles()
16.40 -
16.41 - def set_styles()
16.42 - {
16.43 - Swing_Thread.require()
16.44 - text_area.getPainter.setStyles(styles)
16.45 - }
16.46 -
16.47 -
16.48 - /* wrap_margin -- cf. org.gjt.sp.jedit.textarea.TextArea.propertiesChanged */
16.49 -
16.50 - def wrap_margin(): Int =
16.51 - {
16.52 - val buffer = text_area.getBuffer
16.53 - val painter = text_area.getPainter
16.54 - val font = painter.getFont
16.55 - val font_context = painter.getFontRenderContext
16.56 -
16.57 - val soft_wrap = buffer.getStringProperty("wrap") == "soft"
16.58 - val max = buffer.getIntegerProperty("maxLineLen", 0)
16.59 -
16.60 - if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
16.61 - else if (soft_wrap)
16.62 - painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3
16.63 - else 0
16.64 - }
16.65 -
16.66 -
16.67 - /* chunks */
16.68 -
16.69 - def line_chunks(physical_lines: Set[Int]): Map[Text.Offset, Chunk] =
16.70 - {
16.71 - import scala.collection.JavaConversions._
16.72 -
16.73 - val buffer = text_area.getBuffer
16.74 - val painter = text_area.getPainter
16.75 - val margin = wrap_margin().toFloat
16.76 -
16.77 - val out = new ArrayList[Chunk]
16.78 - val handler = new DisplayTokenHandler
16.79 -
16.80 - var result = Map[Text.Offset, Chunk]()
16.81 - for (line <- physical_lines) {
16.82 - out.clear
16.83 - handler.init(painter.getStyles, painter.getFontRenderContext, painter, out, margin)
16.84 - buffer.markTokens(line, handler)
16.85 -
16.86 - val line_start = buffer.getLineStartOffset(line)
16.87 - for (chunk <- handler.getChunkList.iterator)
16.88 - result += (line_start + chunk.offset -> chunk)
16.89 - }
16.90 - result
16.91 - }
16.92 -
16.93 -
16.94 /* visible line ranges */
16.95
16.96 // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
16.97 @@ -209,7 +144,8 @@
16.98 }
16.99 }
16.100
16.101 - private var highlight_range: Option[(Text.Range, Color)] = None
16.102 + @volatile private var _highlight_range: Option[(Text.Range, Color)] = None
16.103 + def highlight_range(): Option[(Text.Range, Color)] = _highlight_range
16.104
16.105
16.106 /* CONTROL-mouse management */
16.107 @@ -219,12 +155,12 @@
16.108 private def exit_control()
16.109 {
16.110 exit_popup()
16.111 - highlight_range = None
16.112 + _highlight_range = None
16.113 }
16.114
16.115 private val focus_listener = new FocusAdapter {
16.116 override def focusLost(e: FocusEvent) {
16.117 - highlight_range = None // FIXME exit_control !?
16.118 + _highlight_range = None // FIXME exit_control !?
16.119 }
16.120 }
16.121
16.122 @@ -246,93 +182,20 @@
16.123
16.124 if (control) init_popup(snapshot, x, y)
16.125
16.126 - highlight_range map { case (range, _) => invalidate_line_range(range) }
16.127 - highlight_range = if (control) subexp_range(snapshot, x, y) else None
16.128 - highlight_range map { case (range, _) => invalidate_line_range(range) }
16.129 + _highlight_range map { case (range, _) => invalidate_line_range(range) }
16.130 + _highlight_range = if (control) subexp_range(snapshot, x, y) else None
16.131 + _highlight_range map { case (range, _) => invalidate_line_range(range) }
16.132 }
16.133 }
16.134 }
16.135
16.136
16.137 - /* TextArea painters */
16.138 + /* text area painting */
16.139
16.140 - private val background_painter = new TextAreaExtension
16.141 + private val text_area_painter = new Text_Area_Painter(this)
16.142 +
16.143 + private val tooltip_painter = new TextAreaExtension
16.144 {
16.145 - override def paintScreenLineRange(gfx: Graphics2D,
16.146 - first_line: Int, last_line: Int, physical_lines: Array[Int],
16.147 - start: Array[Int], end: Array[Int], y: Int, line_height: Int)
16.148 - {
16.149 - Isabelle.swing_buffer_lock(model.buffer) {
16.150 - val snapshot = model.snapshot()
16.151 - val ascent = text_area.getPainter.getFontMetrics.getAscent
16.152 -
16.153 - for (i <- 0 until physical_lines.length) {
16.154 - if (physical_lines(i) != -1) {
16.155 - val line_range = proper_line_range(start(i), end(i))
16.156 -
16.157 - // background color: status
16.158 - val cmds = snapshot.node.command_range(snapshot.revert(line_range))
16.159 - for {
16.160 - (command, command_start) <- cmds if !command.is_ignored
16.161 - val range = line_range.restrict(snapshot.convert(command.range + command_start))
16.162 - r <- Isabelle.gfx_range(text_area, range)
16.163 - color <- Isabelle_Markup.status_color(snapshot, command)
16.164 - } {
16.165 - gfx.setColor(color)
16.166 - gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
16.167 - }
16.168 -
16.169 - // background color (1): markup
16.170 - for {
16.171 - Text.Info(range, Some(color)) <-
16.172 - snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
16.173 - r <- Isabelle.gfx_range(text_area, range)
16.174 - } {
16.175 - gfx.setColor(color)
16.176 - gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
16.177 - }
16.178 -
16.179 - // background color (2): markup
16.180 - for {
16.181 - Text.Info(range, Some(color)) <-
16.182 - snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
16.183 - r <- Isabelle.gfx_range(text_area, range)
16.184 - } {
16.185 - gfx.setColor(color)
16.186 - gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
16.187 - }
16.188 -
16.189 - // sub-expression highlighting -- potentially from other snapshot
16.190 - highlight_range match {
16.191 - case Some((range, color)) if line_range.overlaps(range) =>
16.192 - Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
16.193 - case None =>
16.194 - case Some(r) =>
16.195 - gfx.setColor(color)
16.196 - gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
16.197 - }
16.198 - case _ =>
16.199 - }
16.200 -
16.201 - // squiggly underline
16.202 - for {
16.203 - Text.Info(range, Some(color)) <-
16.204 - snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
16.205 - r <- Isabelle.gfx_range(text_area, range)
16.206 - } {
16.207 - gfx.setColor(color)
16.208 - val x0 = (r.x / 2) * 2
16.209 - val y0 = r.y + ascent + 1
16.210 - for (x1 <- Range(x0, x0 + r.length, 2)) {
16.211 - val y1 = if (x1 % 4 < 2) y0 else y0 + 1
16.212 - gfx.drawLine(x1, y1, x1 + 1, y1)
16.213 - }
16.214 - }
16.215 - }
16.216 - }
16.217 - }
16.218 - }
16.219 -
16.220 override def getToolTipText(x: Int, y: Int): String =
16.221 {
16.222 Isabelle.swing_buffer_lock(model.buffer) {
16.223 @@ -357,38 +220,6 @@
16.224 }
16.225 }
16.226
16.227 - var use_text_painter = false
16.228 -
16.229 - private val text_painter = new TextAreaExtension
16.230 - {
16.231 - override def paintScreenLineRange(gfx: Graphics2D,
16.232 - first_line: Int, last_line: Int, physical_lines: Array[Int],
16.233 - start: Array[Int], end: Array[Int], y: Int, line_height: Int)
16.234 - {
16.235 - if (use_text_painter) {
16.236 - Isabelle.swing_buffer_lock(model.buffer) {
16.237 - val painter = text_area.getPainter
16.238 - val fm = painter.getFontMetrics
16.239 -
16.240 - val all_chunks = line_chunks(Set[Int]() ++ physical_lines.iterator.filter(i => i != -1))
16.241 -
16.242 - val x0 = text_area.getHorizontalOffset
16.243 - var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
16.244 - for (i <- 0 until physical_lines.length) {
16.245 - if (physical_lines(i) != -1) {
16.246 - all_chunks.get(start(i)) match {
16.247 - case Some(chunk) =>
16.248 - Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR)
16.249 - case None =>
16.250 - }
16.251 - }
16.252 - y0 += line_height
16.253 - }
16.254 - }
16.255 - }
16.256 - }
16.257 - }
16.258 -
16.259 private val gutter_painter = new TextAreaExtension
16.260 {
16.261 override def paintScreenLineRange(gfx: Graphics2D,
16.262 @@ -557,8 +388,8 @@
16.263 private def activate()
16.264 {
16.265 val painter = text_area.getPainter
16.266 - painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
16.267 - painter.addExtension(TextAreaPainter.TEXT_LAYER + 1, text_painter)
16.268 + painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
16.269 + text_area_painter.activate()
16.270 text_area.getGutter.addExtension(gutter_painter)
16.271 text_area.addFocusListener(focus_listener)
16.272 text_area.getView.addWindowListener(window_listener)
16.273 @@ -580,8 +411,8 @@
16.274 text_area.removeCaretListener(caret_listener)
16.275 text_area.removeLeftOfScrollBar(overview)
16.276 text_area.getGutter.removeExtension(gutter_painter)
16.277 - painter.removeExtension(text_painter)
16.278 - painter.removeExtension(background_painter)
16.279 + text_area_painter.deactivate()
16.280 + painter.removeExtension(tooltip_painter)
16.281 exit_popup()
16.282 }
16.283 }
17.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala Wed Jun 15 14:36:41 2011 +0200
17.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala Wed Jun 15 15:11:18 2011 +0200
17.3 @@ -11,6 +11,7 @@
17.4
17.5 import java.awt.Color
17.6
17.7 +import org.lobobrowser.util.gui.ColorFactory
17.8 import org.gjt.sp.jedit.syntax.Token
17.9
17.10
17.11 @@ -18,6 +19,10 @@
17.12 {
17.13 /* physical rendering */
17.14
17.15 + // see http://www.w3schools.com/css/css_colornames.asp
17.16 +
17.17 + def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
17.18 +
17.19 val outdated_color = new Color(240, 240, 240)
17.20 val unfinished_color = new Color(255, 228, 225)
17.21
17.22 @@ -28,6 +33,9 @@
17.23 val bad_color = new Color(255, 106, 106, 100)
17.24 val hilite_color = new Color(255, 204, 102, 100)
17.25
17.26 + val keyword1_color = get_color("#006699")
17.27 + val keyword2_color = get_color("#009966")
17.28 +
17.29 class Icon(val priority: Int, val icon: javax.swing.Icon)
17.30 {
17.31 def >= (that: Icon): Boolean = this.priority >= that.priority
17.32 @@ -100,6 +108,35 @@
17.33 case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
17.34 }
17.35
17.36 + private val foreground_colors: Map[String, Color] =
17.37 + Map(
17.38 + Markup.TCLASS -> get_color("red"),
17.39 + Markup.TFREE -> get_color("#A020F0"),
17.40 + Markup.TVAR -> get_color("#A020F0"),
17.41 + Markup.CONST -> get_color("dimgrey"),
17.42 + Markup.FREE -> get_color("blue"),
17.43 + Markup.SKOLEM -> get_color("#D2691E"),
17.44 + Markup.BOUND -> get_color("green"),
17.45 + Markup.VAR -> get_color("#00009B"),
17.46 + Markup.INNER_STRING -> get_color("#D2691E"),
17.47 + Markup.INNER_COMMENT -> get_color("#8B0000"),
17.48 + Markup.DYNAMIC_FACT -> get_color("yellowgreen"),
17.49 + Markup.LITERAL -> keyword1_color,
17.50 + Markup.ML_KEYWORD -> keyword1_color,
17.51 + Markup.ML_DELIMITER -> get_color("black"),
17.52 + Markup.ML_NUMERAL -> get_color("red"),
17.53 + Markup.ML_CHAR -> get_color("#D2691E"),
17.54 + Markup.ML_STRING -> get_color("#D2691E"),
17.55 + Markup.ML_COMMENT -> get_color("#8B0000"),
17.56 + Markup.ML_MALFORMED -> get_color("#FF6A6A")
17.57 + )
17.58 +
17.59 + val foreground: Markup_Tree.Select[Color] =
17.60 + {
17.61 + case Text.Info(_, XML.Elem(Markup(m, _), _))
17.62 + if foreground_colors.isDefinedAt(m) => foreground_colors(m)
17.63 + }
17.64 +
17.65 val tooltip: Markup_Tree.Select[String] =
17.66 {
17.67 case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\""
17.68 @@ -148,40 +185,9 @@
17.69 private val token_style: Map[String, Byte] =
17.70 {
17.71 import Token._
17.72 + val SUBSCRIPT: Byte = ID_COUNT
17.73 + val SUPERSCRIPT: Byte = ID_COUNT + 1
17.74 Map[String, Byte](
17.75 - // logical entities
17.76 - Markup.TCLASS -> NULL,
17.77 - Markup.TYCON -> NULL,
17.78 - Markup.FIXED -> NULL,
17.79 - Markup.CONST -> LITERAL2,
17.80 - Markup.DYNAMIC_FACT -> LABEL,
17.81 - // inner syntax
17.82 - Markup.TFREE -> NULL,
17.83 - Markup.FREE -> MARKUP,
17.84 - Markup.TVAR -> NULL,
17.85 - Markup.SKOLEM -> COMMENT2,
17.86 - Markup.BOUND -> LABEL,
17.87 - Markup.VAR -> NULL,
17.88 - Markup.NUM -> DIGIT,
17.89 - Markup.FLOAT -> DIGIT,
17.90 - Markup.XNUM -> DIGIT,
17.91 - Markup.XSTR -> LITERAL4,
17.92 - Markup.LITERAL -> OPERATOR,
17.93 - Markup.INNER_COMMENT -> COMMENT1,
17.94 - Markup.SORT -> NULL,
17.95 - Markup.TYP -> NULL,
17.96 - Markup.TERM -> NULL,
17.97 - Markup.PROP -> NULL,
17.98 - // ML syntax
17.99 - Markup.ML_KEYWORD -> KEYWORD1,
17.100 - Markup.ML_DELIMITER -> OPERATOR,
17.101 - Markup.ML_IDENT -> NULL,
17.102 - Markup.ML_TVAR -> NULL,
17.103 - Markup.ML_NUMERAL -> DIGIT,
17.104 - Markup.ML_CHAR -> LITERAL1,
17.105 - Markup.ML_STRING -> LITERAL1,
17.106 - Markup.ML_COMMENT -> COMMENT1,
17.107 - Markup.ML_MALFORMED -> INVALID,
17.108 // embedded source text
17.109 Markup.ML_SOURCE -> COMMENT3,
17.110 Markup.DOC_SOURCE -> COMMENT3,
18.1 --- a/src/Tools/jEdit/src/plugin.scala Wed Jun 15 14:36:41 2011 +0200
18.2 +++ b/src/Tools/jEdit/src/plugin.scala Wed Jun 15 15:11:18 2011 +0200
18.3 @@ -373,11 +373,7 @@
18.4 }
18.5
18.6 case msg: PropertiesChanged =>
18.7 - Swing_Thread.now {
18.8 - Isabelle.setup_tooltips()
18.9 - for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
18.10 - Document_View(text_area).get.extend_styles()
18.11 - }
18.12 + Swing_Thread.now { Isabelle.setup_tooltips() }
18.13 Isabelle.session.global_settings.event(Session.Global_Settings)
18.14
18.15 case _ =>
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala Wed Jun 15 15:11:18 2011 +0200
19.3 @@ -0,0 +1,284 @@
19.4 +/* Title: Tools/jEdit/src/text_area_painter.scala
19.5 + Author: Makarius
19.6 +
19.7 +Painter setup for main jEdit text area.
19.8 +*/
19.9 +
19.10 +package isabelle.jedit
19.11 +
19.12 +
19.13 +import isabelle._
19.14 +
19.15 +import java.awt.Graphics2D
19.16 +import java.util.ArrayList
19.17 +
19.18 +import org.gjt.sp.jedit.Debug
19.19 +import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
19.20 +import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter}
19.21 +
19.22 +
19.23 +class Text_Area_Painter(doc_view: Document_View)
19.24 +{
19.25 + private val model = doc_view.model
19.26 + private val buffer = model.buffer
19.27 + private val text_area = doc_view.text_area
19.28 +
19.29 + private val orig_text_painter: TextAreaExtension =
19.30 + {
19.31 + val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText"
19.32 + text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
19.33 + match {
19.34 + case List(x) => x
19.35 + case _ => error("Expected exactly one " + name)
19.36 + }
19.37 + }
19.38 +
19.39 +
19.40 + /* painter snapshot */
19.41 +
19.42 + @volatile private var _painter_snapshot: Option[Document.Snapshot] = None
19.43 +
19.44 + private def painter_snapshot(): Document.Snapshot =
19.45 + _painter_snapshot match {
19.46 + case Some(snapshot) => snapshot
19.47 + case None => error("Missing document snapshot for text area painter")
19.48 + }
19.49 +
19.50 + private val set_snapshot = new TextAreaExtension
19.51 + {
19.52 + override def paintScreenLineRange(gfx: Graphics2D,
19.53 + first_line: Int, last_line: Int, physical_lines: Array[Int],
19.54 + start: Array[Int], end: Array[Int], y: Int, line_height: Int)
19.55 + {
19.56 + _painter_snapshot = Some(model.snapshot())
19.57 + }
19.58 + }
19.59 +
19.60 + private val reset_snapshot = new TextAreaExtension
19.61 + {
19.62 + override def paintScreenLineRange(gfx: Graphics2D,
19.63 + first_line: Int, last_line: Int, physical_lines: Array[Int],
19.64 + start: Array[Int], end: Array[Int], y: Int, line_height: Int)
19.65 + {
19.66 + _painter_snapshot = None
19.67 + }
19.68 + }
19.69 +
19.70 +
19.71 + /* text background */
19.72 +
19.73 + private val background_painter = new TextAreaExtension
19.74 + {
19.75 + override def paintScreenLineRange(gfx: Graphics2D,
19.76 + first_line: Int, last_line: Int, physical_lines: Array[Int],
19.77 + start: Array[Int], end: Array[Int], y: Int, line_height: Int)
19.78 + {
19.79 + Isabelle.swing_buffer_lock(buffer) {
19.80 + val snapshot = painter_snapshot()
19.81 + val ascent = text_area.getPainter.getFontMetrics.getAscent
19.82 +
19.83 + for (i <- 0 until physical_lines.length) {
19.84 + if (physical_lines(i) != -1) {
19.85 + val line_range = doc_view.proper_line_range(start(i), end(i))
19.86 +
19.87 + // background color: status
19.88 + val cmds = snapshot.node.command_range(snapshot.revert(line_range))
19.89 + for {
19.90 + (command, command_start) <- cmds if !command.is_ignored
19.91 + val range = line_range.restrict(snapshot.convert(command.range + command_start))
19.92 + r <- Isabelle.gfx_range(text_area, range)
19.93 + color <- Isabelle_Markup.status_color(snapshot, command)
19.94 + } {
19.95 + gfx.setColor(color)
19.96 + gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
19.97 + }
19.98 +
19.99 + // background color (1): markup
19.100 + for {
19.101 + Text.Info(range, Some(color)) <-
19.102 + snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
19.103 + r <- Isabelle.gfx_range(text_area, range)
19.104 + } {
19.105 + gfx.setColor(color)
19.106 + gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
19.107 + }
19.108 +
19.109 + // background color (2): markup
19.110 + for {
19.111 + Text.Info(range, Some(color)) <-
19.112 + snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
19.113 + r <- Isabelle.gfx_range(text_area, range)
19.114 + } {
19.115 + gfx.setColor(color)
19.116 + gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
19.117 + }
19.118 +
19.119 + // sub-expression highlighting -- potentially from other snapshot
19.120 + doc_view.highlight_range match {
19.121 + case Some((range, color)) if line_range.overlaps(range) =>
19.122 + Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
19.123 + case None =>
19.124 + case Some(r) =>
19.125 + gfx.setColor(color)
19.126 + gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
19.127 + }
19.128 + case _ =>
19.129 + }
19.130 +
19.131 + // squiggly underline
19.132 + for {
19.133 + Text.Info(range, Some(color)) <-
19.134 + snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
19.135 + r <- Isabelle.gfx_range(text_area, range)
19.136 + } {
19.137 + gfx.setColor(color)
19.138 + val x0 = (r.x / 2) * 2
19.139 + val y0 = r.y + ascent + 1
19.140 + for (x1 <- Range(x0, x0 + r.length, 2)) {
19.141 + val y1 = if (x1 % 4 < 2) y0 else y0 + 1
19.142 + gfx.drawLine(x1, y1, x1 + 1, y1)
19.143 + }
19.144 + }
19.145 + }
19.146 + }
19.147 + }
19.148 + }
19.149 + }
19.150 +
19.151 +
19.152 + /* text */
19.153 +
19.154 + private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
19.155 + {
19.156 + val painter = text_area.getPainter
19.157 + val font = painter.getFont
19.158 + val font_context = painter.getFontRenderContext
19.159 +
19.160 + // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
19.161 + // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
19.162 + val margin =
19.163 + if (buffer.getStringProperty("wrap") != "soft") 0.0f
19.164 + else {
19.165 + val max = buffer.getIntegerProperty("maxLineLen", 0)
19.166 + if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
19.167 + else painter.getWidth - font.getStringBounds(" ", font_context).getWidth.round.toInt * 3
19.168 + }.toFloat
19.169 +
19.170 + val out = new ArrayList[Chunk]
19.171 + val handler = new DisplayTokenHandler
19.172 +
19.173 + var result = Map[Text.Offset, Chunk]()
19.174 + for (line <- physical_lines) {
19.175 + out.clear
19.176 + handler.init(painter.getStyles, font_context, painter, out, margin)
19.177 + buffer.markTokens(line, handler)
19.178 +
19.179 + val line_start = buffer.getLineStartOffset(line)
19.180 + for (i <- 0 until out.size) {
19.181 + val chunk = out.get(i)
19.182 + result += (line_start + chunk.offset -> chunk)
19.183 + }
19.184 + }
19.185 + result
19.186 + }
19.187 +
19.188 + private def paint_chunk_list(gfx: Graphics2D,
19.189 + offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
19.190 + {
19.191 + val clip_rect = gfx.getClipBounds
19.192 + val font_context = text_area.getPainter.getFontRenderContext
19.193 +
19.194 + var w = 0.0f
19.195 + var chunk_offset = offset
19.196 + var chunk = head
19.197 + while (chunk != null) {
19.198 + val chunk_length = if (chunk.str == null) 0 else chunk.str.length
19.199 +
19.200 + if (x + w + chunk.width > clip_rect.x &&
19.201 + x + w < clip_rect.x + clip_rect.width &&
19.202 + chunk.accessable && chunk.visible)
19.203 + {
19.204 + val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk_length)
19.205 + val chunk_font = chunk.style.getFont
19.206 + val chunk_color = chunk.style.getForegroundColor
19.207 +
19.208 + val markup = painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
19.209 +
19.210 + gfx.setFont(chunk_font)
19.211 + if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
19.212 + markup.forall(info => info.info.isEmpty)) {
19.213 + gfx.setColor(chunk_color)
19.214 + gfx.drawGlyphVector(chunk.gv, x + w, y)
19.215 + }
19.216 + else {
19.217 + var x1 = x + w
19.218 + for (Text.Info(range, info) <- markup) {
19.219 + val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
19.220 + gfx.setColor(info.getOrElse(chunk_color))
19.221 + gfx.drawString(str, x1.toInt, y.toInt)
19.222 + x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
19.223 + }
19.224 + }
19.225 + }
19.226 + w += chunk.width
19.227 + chunk_offset += chunk_length
19.228 + chunk = chunk.next.asInstanceOf[Chunk]
19.229 + }
19.230 + w
19.231 + }
19.232 +
19.233 + private val text_painter = new TextAreaExtension
19.234 + {
19.235 + override def paintScreenLineRange(gfx: Graphics2D,
19.236 + first_line: Int, last_line: Int, physical_lines: Array[Int],
19.237 + start: Array[Int], end: Array[Int], y: Int, line_height: Int)
19.238 + {
19.239 + Isabelle.swing_buffer_lock(buffer) {
19.240 + val clip = gfx.getClip
19.241 + val x0 = text_area.getHorizontalOffset
19.242 + val fm = text_area.getPainter.getFontMetrics
19.243 + var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
19.244 +
19.245 + val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
19.246 + for (i <- 0 until physical_lines.length) {
19.247 + if (physical_lines(i) != -1) {
19.248 + infos.get(start(i)) match {
19.249 + case Some(chunk) =>
19.250 + val w = paint_chunk_list(gfx, start(i), chunk, x0, y0).toInt
19.251 + gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
19.252 + orig_text_painter.paintValidLine(gfx,
19.253 + first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
19.254 + gfx.setClip(clip)
19.255 + case None =>
19.256 + }
19.257 + }
19.258 + y0 += line_height
19.259 + }
19.260 + }
19.261 + }
19.262 + }
19.263 +
19.264 +
19.265 + /* activation */
19.266 +
19.267 + def activate()
19.268 + {
19.269 + val painter = text_area.getPainter
19.270 + painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot)
19.271 + painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
19.272 + painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
19.273 + painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
19.274 + painter.removeExtension(orig_text_painter)
19.275 + }
19.276 +
19.277 + def deactivate()
19.278 + {
19.279 + val painter = text_area.getPainter
19.280 + painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
19.281 + painter.removeExtension(reset_snapshot)
19.282 + painter.removeExtension(text_painter)
19.283 + painter.removeExtension(background_painter)
19.284 + painter.removeExtension(set_snapshot)
19.285 + }
19.286 +}
19.287 +