--- a/Admin/isatest/isatest-makedist Wed Jun 15 14:36:41 2011 +0200
+++ b/Admin/isatest/isatest-makedist Wed Jun 15 15:11:18 2011 +0200
@@ -98,7 +98,7 @@
## spawn test runs
-$SSH macbroy20 "$MAKEALL $HOME/settings/at-poly-test"
+$SSH macbroy21 "$MAKEALL $HOME/settings/at-poly-test"
# give test some time to copy settings and start
sleep 15
$SSH macbroy28 "$MAKEALL $HOME/settings/at-poly"
--- a/Admin/isatest/settings/at-poly-test Wed Jun 15 14:36:41 2011 +0200
+++ b/Admin/isatest/settings/at-poly-test Wed Jun 15 15:11:18 2011 +0200
@@ -24,7 +24,7 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true"
-ISABELLE_GHC="/usr/bin/ghc"
+ISABELLE_GHC="/home/isabelle/contrib_devel/ghc/x86-linux/ghc"
ISABELLE_OCAML="/home/isabelle/contrib_devel/ocaml/x86-linux/ocaml"
ISABELLE_SWIPL="/home/isabelle/contrib_devel/swipl/bin/swipl"
--- a/doc-src/IsarRef/Thy/Generic.thy Wed Jun 15 14:36:41 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Wed Jun 15 15:11:18 2011 +0200
@@ -64,6 +64,8 @@
@{method_def erule}@{text "\<^sup>*"} & : & @{text method} \\
@{method_def drule}@{text "\<^sup>*"} & : & @{text method} \\
@{method_def frule}@{text "\<^sup>*"} & : & @{text method} \\
+ @{method_def intro} & : & @{text method} \\
+ @{method_def elim} & : & @{text method} \\
@{method_def succeed} & : & @{text method} \\
@{method_def fail} & : & @{text method} \\
\end{matharray}
@@ -73,6 +75,8 @@
;
(@@{method erule} | @@{method drule} | @@{method frule})
('(' @{syntax nat} ')')? @{syntax thmrefs}
+ ;
+ (@@{method intro} | @@{method elim}) @{syntax thmrefs}?
"}
\begin{description}
@@ -103,6 +107,12 @@
the plain @{method rule} method, with forward chaining of current
facts.
+ \item @{method intro} and @{method elim} repeatedly refine some goal
+ by intro- or elim-resolution, after having inserted any chained
+ facts. Exactly the rules given as arguments are taken into account;
+ this allows fine-tuned decomposition of a proof problem, in contrast
+ to common automated tools.
+
\item @{method succeed} yields a single (unchanged) result; it is
the identity of the ``@{text ","}'' method combinator (cf.\
\secref{sec:proof-meth}).
@@ -879,6 +889,39 @@
*}
+subsection {* Structured methods *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{method_def rule} & : & @{text method} \\
+ @{method_def contradiction} & : & @{text method} \\
+ \end{matharray}
+
+ @{rail "
+ @@{method rule} @{syntax thmrefs}?
+ "}
+
+ \begin{description}
+
+ \item @{method rule} as offered by the Classical Reasoner is a
+ refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
+ versions work the same, but the classical version observes the
+ classical rule context in addition to that of Isabelle/Pure.
+
+ Common object logics (HOL, ZF, etc.) declare a rich collection of
+ classical rules (even if these would qualify as intuitionistic
+ ones), but only few declarations to the rule context of
+ Isabelle/Pure (\secref{sec:pure-meth-att}).
+
+ \item @{method contradiction} solves some goal by contradiction,
+ deriving any result from both @{text "\<not> A"} and @{text A}. Chained
+ facts, which are guaranteed to participate, may appear in either
+ order.
+
+ \end{description}
+*}
+
+
subsection {* Automated methods *}
text {*
@@ -892,6 +935,7 @@
@{method_def fastsimp} & : & @{text method} \\
@{method_def slowsimp} & : & @{text method} \\
@{method_def bestsimp} & : & @{text method} \\
+ @{method_def deepen} & : & @{text method} \\
\end{matharray}
@{rail "
@@ -906,6 +950,8 @@
(@@{method fastsimp} | @@{method slowsimp} | @@{method bestsimp})
(@{syntax clasimpmod} * )
;
+ @@{method deepen} (@{syntax nat} ?) (@{syntax clamod} * )
+ ;
@{syntax_def clamod}:
(('intro' | 'elim' | 'dest') ('!' | () | '?') | 'del') ':' @{syntax thmrefs}
;
@@ -990,6 +1036,14 @@
like @{method fast}, @{method slow}, @{method best}, respectively,
but use the Simplifier as additional wrapper.
+ \item @{method deepen} works by exhaustive search up to a certain
+ depth. The start depth is 4 (unless specified explicitly), and the
+ depth is increased iteratively up to 10. Unsafe rules are modified
+ to preserve the formula they act on, so that it be used repeatedly.
+ This method can prove more goals than @{method fast}, but is much
+ slower, for example if the assumptions have many universal
+ quantifiers.
+
\end{description}
Any of the above methods support additional modifiers of the context
@@ -1025,13 +1079,8 @@
\item @{method safe} repeatedly performs safe steps on all subgoals.
It is deterministic, with at most one outcome.
- \item @{method clarify} performs a series of safe steps as follows.
-
- No splitting step is applied; for example, the subgoal @{text "A \<and>
- B"} is left as a conjunction. Proof by assumption, Modus Ponens,
- etc., may be performed provided they do not instantiate unknowns.
- Assumptions of the form @{text "x = t"} may be eliminated. The safe
- wrapper tactical is applied.
+ \item @{method clarify} performs a series of safe steps without
+ splitting subgoals; see also @{ML clarify_step_tac}.
\item @{method clarsimp} acts like @{method clarify}, but also does
simplification. Note that if the Simplifier context includes a
@@ -1041,42 +1090,47 @@
*}
-subsection {* Structured proof methods *}
+subsection {* Single-step tactics *}
text {*
\begin{matharray}{rcl}
- @{method_def rule} & : & @{text method} \\
- @{method_def contradiction} & : & @{text method} \\
- @{method_def intro} & : & @{text method} \\
- @{method_def elim} & : & @{text method} \\
+ @{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\
+ @{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\
+ @{index_ML step_tac: "Proof.context -> int -> tactic"} \\
+ @{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\
+ @{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\
\end{matharray}
- @{rail "
- (@@{method rule} | @@{method intro} | @@{method elim}) @{syntax thmrefs}?
- "}
+ These are the primitive tactics behind the (semi)automated proof
+ methods of the Classical Reasoner. By calling them yourself, you
+ can execute these procedures one step at a time.
\begin{description}
- \item @{method rule} as offered by the Classical Reasoner is a
- refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
- versions work the same, but the classical version observes the
- classical rule context in addition to that of Isabelle/Pure.
+ \item @{ML safe_step_tac}~@{text "ctxt i"} performs a safe step on
+ subgoal @{text i}. The safe wrapper tacticals are applied to a
+ tactic that may include proof by assumption or Modus Ponens (taking
+ care not to instantiate unknowns), or substitution.
- Common object logics (HOL, ZF, etc.) declare a rich collection of
- classical rules (even if these would qualify as intuitionistic
- ones), but only few declarations to the rule context of
- Isabelle/Pure (\secref{sec:pure-meth-att}).
+ \item @{ML inst_step_tac} is like @{ML safe_step_tac}, but allows
+ unknowns to be instantiated.
- \item @{method contradiction} solves some goal by contradiction,
- deriving any result from both @{text "\<not> A"} and @{text A}. Chained
- facts, which are guaranteed to participate, may appear in either
- order.
+ \item @{ML step_tac}~@{text "ctxt i"} is the basic step of the proof
+ procedure. The unsafe wrapper tacticals are applied to a tactic
+ that tries @{ML safe_tac}, @{ML inst_step_tac}, or applies an unsafe
+ rule from the context.
- \item @{method intro} and @{method elim} repeatedly refine some goal
- by intro- or elim-resolution, after having inserted any chained
- facts. Exactly the rules given as arguments are taken into account;
- this allows fine-tuned decomposition of a proof problem, in contrast
- to common automated tools.
+ \item @{ML slow_step_tac} resembles @{ML step_tac}, but allows
+ backtracking between using safe rules with instantiation (@{ML
+ inst_step_tac}) and using unsafe rules. The resulting search space
+ is larger.
+
+ \item @{ML clarify_step_tac}~@{text "ctxt i"} performs a safe step
+ on subgoal @{text i}. No splitting step is applied; for example,
+ the subgoal @{text "A \<and> B"} is left as a conjunction. Proof by
+ assumption, Modus Ponens, etc., may be performed provided they do
+ not instantiate unknowns. Assumptions of the form @{text "x = t"}
+ may be eliminated. The safe wrapper tactical is applied.
\end{description}
*}
--- a/doc-src/IsarRef/Thy/document/Generic.tex Wed Jun 15 14:36:41 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Wed Jun 15 15:11:18 2011 +0200
@@ -123,6 +123,8 @@
\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} \\
\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} \\
\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} \\
+ \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
+ \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
\indexdef{}{method}{succeed}\hypertarget{method.succeed}{\hyperlink{method.succeed}{\mbox{\isa{succeed}}}} & : & \isa{method} \\
\indexdef{}{method}{fail}\hypertarget{method.fail}{\hyperlink{method.fail}{\mbox{\isa{fail}}}} & : & \isa{method} \\
\end{matharray}
@@ -154,6 +156,17 @@
\rail@endbar
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@end
+\rail@begin{2}{}
+\rail@bar
+\rail@term{\hyperlink{method.intro}{\mbox{\isa{intro}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{method.elim}{\mbox{\isa{elim}}}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@endbar
+\rail@end
\end{railoutput}
@@ -182,6 +195,12 @@
the plain \hyperlink{method.rule}{\mbox{\isa{rule}}} method, with forward chaining of current
facts.
+ \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
+ by intro- or elim-resolution, after having inserted any chained
+ facts. Exactly the rules given as arguments are taken into account;
+ this allows fine-tuned decomposition of a proof problem, in contrast
+ to common automated tools.
+
\item \hyperlink{method.succeed}{\mbox{\isa{succeed}}} yields a single (unchanged) result; it is
the identity of the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{22}{\isachardoublequote}}}'' method combinator (cf.\
\secref{sec:proof-meth}).
@@ -1311,6 +1330,48 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Structured methods%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
+ \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
+ \end{matharray}
+
+ \begin{railoutput}
+\rail@begin{2}{}
+\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
+
+
+ \begin{description}
+
+ \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
+ refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
+ versions work the same, but the classical version observes the
+ classical rule context in addition to that of Isabelle/Pure.
+
+ Common object logics (HOL, ZF, etc.) declare a rich collection of
+ classical rules (even if these would qualify as intuitionistic
+ ones), but only few declarations to the rule context of
+ Isabelle/Pure (\secref{sec:pure-meth-att}).
+
+ \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
+ deriving any result from both \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequote}}} and \isa{A}. Chained
+ facts, which are guaranteed to participate, may appear in either
+ order.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsubsection{Automated methods%
}
\isamarkuptrue%
@@ -1326,6 +1387,7 @@
\indexdef{}{method}{fastsimp}\hypertarget{method.fastsimp}{\hyperlink{method.fastsimp}{\mbox{\isa{fastsimp}}}} & : & \isa{method} \\
\indexdef{}{method}{slowsimp}\hypertarget{method.slowsimp}{\hyperlink{method.slowsimp}{\mbox{\isa{slowsimp}}}} & : & \isa{method} \\
\indexdef{}{method}{bestsimp}\hypertarget{method.bestsimp}{\hyperlink{method.bestsimp}{\mbox{\isa{bestsimp}}}} & : & \isa{method} \\
+ \indexdef{}{method}{deepen}\hypertarget{method.deepen}{\hyperlink{method.deepen}{\mbox{\isa{deepen}}}} & : & \isa{method} \\
\end{matharray}
\begin{railoutput}
@@ -1385,6 +1447,17 @@
\rail@cnont{\hyperlink{syntax.clasimpmod}{\mbox{\isa{clasimpmod}}}}[]
\rail@endplus
\rail@end
+\rail@begin{2}{}
+\rail@term{\hyperlink{method.deepen}{\mbox{\isa{deepen}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
+\rail@endbar
+\rail@plus
+\rail@nextplus{1}
+\rail@cnont{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}[]
+\rail@endplus
+\rail@end
\rail@begin{4}{\indexdef{}{syntax}{clamod}\hypertarget{syntax.clamod}{\hyperlink{syntax.clamod}{\mbox{\isa{clamod}}}}}
\rail@bar
\rail@bar
@@ -1541,6 +1614,14 @@
like \hyperlink{method.fast}{\mbox{\isa{fast}}}, \hyperlink{method.slow}{\mbox{\isa{slow}}}, \hyperlink{method.best}{\mbox{\isa{best}}}, respectively,
but use the Simplifier as additional wrapper.
+ \item \hyperlink{method.deepen}{\mbox{\isa{deepen}}} works by exhaustive search up to a certain
+ depth. The start depth is 4 (unless specified explicitly), and the
+ depth is increased iteratively up to 10. Unsafe rules are modified
+ to preserve the formula they act on, so that it be used repeatedly.
+ This method can prove more goals than \hyperlink{method.fast}{\mbox{\isa{fast}}}, but is much
+ slower, for example if the assumptions have many universal
+ quantifiers.
+
\end{description}
Any of the above methods support additional modifiers of the context
@@ -1595,12 +1676,8 @@
\item \hyperlink{method.safe}{\mbox{\isa{safe}}} repeatedly performs safe steps on all subgoals.
It is deterministic, with at most one outcome.
- \item \hyperlink{method.clarify}{\mbox{\isa{clarify}}} performs a series of safe steps as follows.
-
- 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,
- etc., may be performed provided they do not instantiate unknowns.
- Assumptions of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} may be eliminated. The safe
- wrapper tactical is applied.
+ \item \hyperlink{method.clarify}{\mbox{\isa{clarify}}} performs a series of safe steps without
+ splitting subgoals; see also \verb|clarify_step_tac|.
\item \hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}} acts like \hyperlink{method.clarify}{\mbox{\isa{clarify}}}, but also does
simplification. Note that if the Simplifier context includes a
@@ -1610,57 +1687,48 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Structured proof methods%
+\isamarkupsubsection{Single-step tactics%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
- \indexdef{}{method}{rule}\hypertarget{method.rule}{\hyperlink{method.rule}{\mbox{\isa{rule}}}} & : & \isa{method} \\
- \indexdef{}{method}{contradiction}\hypertarget{method.contradiction}{\hyperlink{method.contradiction}{\mbox{\isa{contradiction}}}} & : & \isa{method} \\
- \indexdef{}{method}{intro}\hypertarget{method.intro}{\hyperlink{method.intro}{\mbox{\isa{intro}}}} & : & \isa{method} \\
- \indexdef{}{method}{elim}\hypertarget{method.elim}{\hyperlink{method.elim}{\mbox{\isa{elim}}}} & : & \isa{method} \\
+ \indexdef{}{ML}{safe\_step\_tac}\verb|safe_step_tac: Proof.context -> int -> tactic| \\
+ \indexdef{}{ML}{inst\_step\_tac}\verb|inst_step_tac: Proof.context -> int -> tactic| \\
+ \indexdef{}{ML}{step\_tac}\verb|step_tac: Proof.context -> int -> tactic| \\
+ \indexdef{}{ML}{slow\_step\_tac}\verb|slow_step_tac: Proof.context -> int -> tactic| \\
+ \indexdef{}{ML}{clarify\_step\_tac}\verb|clarify_step_tac: Proof.context -> int -> tactic| \\
\end{matharray}
- \begin{railoutput}
-\rail@begin{3}{}
-\rail@bar
-\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
-\rail@nextbar{1}
-\rail@term{\hyperlink{method.intro}{\mbox{\isa{intro}}}}[]
-\rail@nextbar{2}
-\rail@term{\hyperlink{method.elim}{\mbox{\isa{elim}}}}[]
-\rail@endbar
-\rail@bar
-\rail@nextbar{1}
-\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
-\rail@endbar
-\rail@end
-\end{railoutput}
-
+ These are the primitive tactics behind the (semi)automated proof
+ methods of the Classical Reasoner. By calling them yourself, you
+ can execute these procedures one step at a time.
\begin{description}
- \item \hyperlink{method.rule}{\mbox{\isa{rule}}} as offered by the Classical Reasoner is a
- refinement over the Pure one (see \secref{sec:pure-meth-att}). Both
- versions work the same, but the classical version observes the
- classical rule context in addition to that of Isabelle/Pure.
+ \item \verb|safe_step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} performs a safe step on
+ subgoal \isa{i}. The safe wrapper tacticals are applied to a
+ tactic that may include proof by assumption or Modus Ponens (taking
+ care not to instantiate unknowns), or substitution.
- Common object logics (HOL, ZF, etc.) declare a rich collection of
- classical rules (even if these would qualify as intuitionistic
- ones), but only few declarations to the rule context of
- Isabelle/Pure (\secref{sec:pure-meth-att}).
+ \item \verb|inst_step_tac| is like \verb|safe_step_tac|, but allows
+ unknowns to be instantiated.
- \item \hyperlink{method.contradiction}{\mbox{\isa{contradiction}}} solves some goal by contradiction,
- deriving any result from both \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequote}}} and \isa{A}. Chained
- facts, which are guaranteed to participate, may appear in either
- order.
+ \item \verb|step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} is the basic step of the proof
+ procedure. The unsafe wrapper tacticals are applied to a tactic
+ that tries \verb|safe_tac|, \verb|inst_step_tac|, or applies an unsafe
+ rule from the context.
- \item \hyperlink{method.intro}{\mbox{\isa{intro}}} and \hyperlink{method.elim}{\mbox{\isa{elim}}} repeatedly refine some goal
- by intro- or elim-resolution, after having inserted any chained
- facts. Exactly the rules given as arguments are taken into account;
- this allows fine-tuned decomposition of a proof problem, in contrast
- to common automated tools.
+ \item \verb|slow_step_tac| resembles \verb|step_tac|, but allows
+ backtracking between using safe rules with instantiation (\verb|inst_step_tac|) and using unsafe rules. The resulting search space
+ is larger.
+
+ \item \verb|clarify_step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} performs a safe step
+ on subgoal \isa{i}. 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, etc., may be performed provided they do
+ not instantiate unknowns. Assumptions of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}}
+ may be eliminated. The safe wrapper tactical is applied.
\end{description}%
\end{isamarkuptext}%
--- a/doc-src/Ref/classical.tex Wed Jun 15 14:36:41 2011 +0200
+++ b/doc-src/Ref/classical.tex Wed Jun 15 15:11:18 2011 +0200
@@ -125,21 +125,6 @@
\section{The classical tactics}
-\subsection{Semi-automatic tactics}
-\begin{ttbox}
-clarify_step_tac : claset -> int -> tactic
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
- subgoal~$i$. No splitting step is applied; for example, the subgoal $A\conj
- B$ is left as a conjunction. Proof by assumption, Modus Ponens, etc., may be
- performed provided they do not instantiate unknowns. Assumptions of the
- form $x=t$ may be eliminated. The user-supplied safe wrapper tactical is
- applied.
-\end{ttdescription}
-
-
\subsection{Other classical tactics}
\begin{ttbox}
slow_best_tac : claset -> int -> tactic
@@ -151,58 +136,6 @@
\end{ttdescription}
-\subsection{Depth-limited automatic tactics}
-\begin{ttbox}
-depth_tac : claset -> int -> int -> tactic
-deepen_tac : claset -> int -> int -> tactic
-\end{ttbox}
-These work by exhaustive search up to a specified depth. Unsafe rules are
-modified to preserve the formula they act on, so that it be used repeatedly.
-They can prove more goals than \texttt{fast_tac} can but are much
-slower, for example if the assumptions have many universal quantifiers.
-
-The depth limits the number of unsafe steps. If you can estimate the minimum
-number of unsafe steps needed, supply this value as~$m$ to save time.
-\begin{ttdescription}
-\item[\ttindexbold{depth_tac} $cs$ $m$ $i$]
-tries to prove subgoal~$i$ by exhaustive search up to depth~$m$.
-
-\item[\ttindexbold{deepen_tac} $cs$ $m$ $i$]
-tries to prove subgoal~$i$ by iterative deepening. It calls \texttt{depth_tac}
-repeatedly with increasing depths, starting with~$m$.
-\end{ttdescription}
-
-
-\subsection{Single-step tactics}
-\begin{ttbox}
-safe_step_tac : claset -> int -> tactic
-inst_step_tac : claset -> int -> tactic
-step_tac : claset -> int -> tactic
-slow_step_tac : claset -> int -> tactic
-\end{ttbox}
-The automatic proof procedures call these tactics. By calling them
-yourself, you can execute these procedures one step at a time.
-\begin{ttdescription}
-\item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
- subgoal~$i$. The safe wrapper tacticals are applied to a tactic that may
- include proof by assumption or Modus Ponens (taking care not to instantiate
- unknowns), or substitution.
-
-\item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac},
-but allows unknowns to be instantiated.
-
-\item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof
- procedure. The unsafe wrapper tacticals are applied to a tactic that tries
- \texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule
- from~$cs$.
-
-\item[\ttindexbold{slow_step_tac}]
- resembles \texttt{step_tac}, but allows backtracking between using safe
- rules with instantiation (\texttt{inst_step_tac}) and using unsafe rules.
- The resulting search space is larger.
-\end{ttdescription}
-
-
\subsection{Other useful tactics}
\index{tactics!for contradiction}
\index{tactics!for Modus Ponens}
--- a/src/HOL/Library/Executable_Set.thy Wed Jun 15 14:36:41 2011 +0200
+++ b/src/HOL/Library/Executable_Set.thy Wed Jun 15 15:11:18 2011 +0200
@@ -12,7 +12,7 @@
text {*
This is just an ad-hoc hack which will rarely give you what you want.
For the moment, whenever you need executable sets, consider using
- type @{text fset} from theory @{text Cset}.
+ type @{text Cset.set} from theory @{text Cset}.
*}
declare mem_def [code del]
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle Wed Jun 15 14:36:41 2011 +0200
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Wed Jun 15 15:11:18 2011 +0200
@@ -90,7 +90,7 @@
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\" #> Config.put Quickcheck.finite_types false) \"exhaustive_nft\",
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"narrowing\" #> Config.put Quickcheck.finite_types false) \"narrowing\",
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"narrowing\" #> Config.put Quickcheck.finite_types false
- #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ int}])))) \"narrowing_nat\"
+ #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\"
(* MutabelleExtra.nitpick_mtd *)
]
*}
--- a/src/HOL/Quickcheck_Narrowing.thy Wed Jun 15 14:36:41 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy Wed Jun 15 15:11:18 2011 +0200
@@ -207,14 +207,6 @@
subsubsection {* Narrowing's deep representation of types and terms *}
datatype narrowing_type = SumOfProd "narrowing_type list list"
-text {*
-The definition of the automatically derived equal type class instance for @{typ narrowing_type}
-causes an error in the OCaml serializer.
-For the moment, we delete this equation manually because we do not require an executable equality
-on this type anyway.
-*}
-declare Quickcheck_Narrowing.equal_narrowing_type_def[code del]
-
datatype narrowing_term = Var "code_int list" narrowing_type | Ctr code_int "narrowing_term list"
datatype 'a cons = C narrowing_type "(narrowing_term list => 'a) list"
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Jun 15 14:36:41 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Jun 15 15:11:18 2011 +0200
@@ -209,6 +209,10 @@
val path = Path.append (Path.explode "~/.isabelle") (Path.basic (name ^ serial_string ()))
val _ = Isabelle_System.mkdirs path;
in Exn.release (Exn.capture f path) end;
+
+fun elapsed_time description e =
+ let val ({elapsed, ...}, result) = Timing.timing e ()
+ in (result, (description, Time.toMilliseconds elapsed)) end
fun value (contains_existentials, (quiet, size)) ctxt (get, put, put_ml) (code, value_name) =
let
@@ -237,20 +241,23 @@
val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
(space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
" -o " ^ executable ^ ";"
+ val (result, compilation_time) = elapsed_time "Haskell compilation" (fn () => bash cmd)
val _ = if bash cmd <> 0 then error "Compilation with GHC failed" else ()
- fun with_size k =
+ fun with_size k exec_times =
if k > size then
- NONE
+ (NONE, exec_times)
else
let
val _ = message ("Test data size: " ^ string_of_int k)
- val (response, _) = bash_output (executable ^ " " ^ string_of_int k)
+ val ((response, _), exec_time) = elapsed_time ("execution of size " ^ string_of_int k)
+ (fn () => bash_output (executable ^ " " ^ string_of_int k))
in
- if response = "NONE\n" then with_size (k + 1) else SOME response
+ if response = "NONE\n" then with_size (k + 1) (exec_time :: exec_times)
+ else (SOME response, exec_time :: exec_times)
end
- in case with_size 0 of
- NONE => NONE
- | SOME response =>
+ in case with_size 0 [compilation_time] of
+ (NONE, exec_times) => (NONE, exec_times)
+ | (SOME response, exec_times) =>
let
val output_value = the_default "NONE"
(try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
@@ -260,7 +267,7 @@
val ctxt' = ctxt
|> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
|> Context.proof_map (exec false ml_code);
- in get ctxt' () end
+ in (get ctxt' (), exec_times) end
end
in with_tmp_dir tmp_prefix run end;
@@ -389,14 +396,14 @@
val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt')
- val result = dynamic_value_strict (true, opts)
+ val (result, timings) = dynamic_value_strict (true, opts)
(Existential_Counterexample.get, Existential_Counterexample.put,
"Narrowing_Generators.put_existential_counterexample")
- thy' (Option.map o map_counterexample) (mk_property qs prop_def')
+ thy' (apfst o Option.map o map_counterexample) (mk_property qs prop_def')
val result' = Option.map (mk_terms ctxt' (fst (strip_quantifiers pnf_t))) result
in
Quickcheck.Result {counterexample = result', evaluation_terms = Option.map (K []) result,
- timings = [], reports = []}
+ timings = timings, reports = []}
end
else
let
@@ -405,12 +412,12 @@
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
fun ensure_testable t =
Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
- val result = dynamic_value_strict (false, opts)
+ val (result, timings) = dynamic_value_strict (false, opts)
(Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
- thy (Option.map o map) (ensure_testable (finitize t'))
+ thy (apfst o Option.map o map) (ensure_testable (finitize t'))
in
Quickcheck.Result {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) result,
- evaluation_terms = Option.map (K []) result, timings = [], reports = []}
+ evaluation_terms = Option.map (K []) result, timings = timings, reports = []}
end
end;
--- a/src/HOL/Tools/SMT/smt_datatypes.ML Wed Jun 15 14:36:41 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_datatypes.ML Wed Jun 15 15:11:18 2011 +0200
@@ -32,12 +32,11 @@
val vars = the (get_first get_vars descr) ~~ Ts
val lookup_var = the o AList.lookup (op =) vars
- val dTs = map (apsnd (fn (m, vs, _) => Type (m, map lookup_var vs))) descr
- val lookup_typ = the o AList.lookup (op =) dTs
-
fun typ_of (dt as Datatype.DtTFree _) = lookup_var dt
- | typ_of (Datatype.DtType (n, dts)) = Type (n, map typ_of dts)
- | typ_of (Datatype.DtRec i) = lookup_typ i
+ | typ_of (Datatype.DtType (m, dts)) = Type (m, map typ_of dts)
+ | typ_of (Datatype.DtRec i) =
+ the (AList.lookup (op =) descr i)
+ |> (fn (m, dts, _) => Type (m, map typ_of dts))
fun mk_constr T (m, dts) ctxt =
let
@@ -48,7 +47,7 @@
fun mk_decl (i, (_, _, constrs)) ctxt =
let
- val T = lookup_typ i
+ val T = typ_of (Datatype.DtRec i)
val (css, ctxt') = fold_map (mk_constr T) constrs ctxt
in ((T, css), ctxt') end
@@ -87,6 +86,7 @@
(* collection of declarations *)
fun declared declss T = exists (exists (equal T o fst)) declss
+fun declared' dss T = exists (exists (equal T o fst) o snd) dss
fun get_decls T n Ts ctxt =
let val thy = Proof_Context.theory_of ctxt
@@ -104,13 +104,15 @@
fun add_decls T (declss, ctxt) =
let
+ fun depends Ts ds = exists (member (op =) (map fst ds)) Ts
+
fun add (TFree _) = I
| add (TVar _) = I
| add (T as Type (@{type_name fun}, _)) =
fold add (Term.body_type T :: Term.binder_types T)
| add @{typ bool} = I
| add (T as Type (n, Ts)) = (fn (dss, ctxt1) =>
- if declared declss T orelse declared dss T then (dss, ctxt1)
+ if declared declss T orelse declared' dss T then (dss, ctxt1)
else if SMT_Builtin.is_builtin_typ_ext ctxt1 T then (dss, ctxt1)
else
(case get_decls T n Ts ctxt1 of
@@ -120,7 +122,13 @@
val constrTs =
maps (map (snd o Term.dest_Const o fst) o snd) ds
val Us = fold (union (op =) o Term.binder_types) constrTs []
- in fold add Us (ds :: dss, ctxt2) end))
- in add T ([], ctxt) |>> append declss end
+
+ fun ins [] = [(Us, ds)]
+ | ins ((Uds as (Us', _)) :: Udss) =
+ if depends Us' ds then (Us, ds) :: Uds :: Udss
+ else Uds :: ins Udss
+ in fold add Us (ins dss, ctxt2) end))
+ in add T ([], ctxt) |>> append declss o map snd end
+
end
--- a/src/HOL/Tools/SMT/smt_translate.ML Wed Jun 15 14:36:41 2011 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML Wed Jun 15 15:11:18 2011 +0200
@@ -160,7 +160,6 @@
Termtab.update (constr, length selects) #>
fold (Termtab.update o rpair 1) selects
val funcs = fold (fold (fold add o snd)) declss Termtab.empty
-
in ((funcs, declss', tr_context', ctxt'), ts) end
(* FIXME: also return necessary datatype and record theorems *)
@@ -344,11 +343,14 @@
in fst (fold app ts2 (Term.list_comb (t, ts1), U)) end
in
-fun intro_explicit_application ctxt ts =
+fun intro_explicit_application ctxt funcs ts =
let
val (arities, types) = fold min_arities ts (Termtab.empty, Typtab.empty)
val arities' = Termtab.map (minimize types) arities
- fun apply' t = apply (the (Termtab.lookup arities' t)) t
+
+ fun app_func t T ts =
+ if is_some (Termtab.lookup funcs t) then Term.list_comb (t, ts)
+ else apply (the (Termtab.lookup arities' t)) t T ts
fun traverse Ts t =
(case Term.strip_comb t of
@@ -359,8 +361,8 @@
| (u as Const (c as (_, T)), ts) =>
(case SMT_Builtin.dest_builtin ctxt c ts of
SOME (_, _, us, mk) => mk (map (traverse Ts) us)
- | NONE => apply' u T (map (traverse Ts) ts))
- | (u as Free (_, T), ts) => apply' u T (map (traverse Ts) ts)
+ | NONE => app_func u T (map (traverse Ts) ts))
+ | (u as Free (_, T), ts) => app_func u T (map (traverse Ts) ts)
| (u as Bound i, ts) => apply 0 u (nth Ts i) (map (traverse Ts) ts)
| (Abs (n, T, u), ts) => traverses Ts (Abs (n, T, traverse (T::Ts) u)) ts
| (u, ts) => traverses Ts u ts)
@@ -586,7 +588,7 @@
ts2
|> eta_expand ctxt1 is_fol funcs
|> lift_lambdas ctxt1
- |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1)
+ |-> (fn ctxt1' => pair ctxt1' o intro_explicit_application ctxt1 funcs)
val ((rewrite_rules, extra_thms, builtin), ts4) =
(if is_fol then folify ctxt2 else pair ([], [], I)) ts3
--- a/src/Pure/General/markup.scala Wed Jun 15 14:36:41 2011 +0200
+++ b/src/Pure/General/markup.scala Wed Jun 15 15:11:18 2011 +0200
@@ -167,6 +167,7 @@
val XNUM = "xnum"
val XSTR = "xstr"
val LITERAL = "literal"
+ val INNER_STRING = "inner_string"
val INNER_COMMENT = "inner_comment"
val TOKEN_RANGE = "token_range"
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Jun 15 14:36:41 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed Jun 15 15:11:18 2011 +0200
@@ -23,6 +23,7 @@
"src/raw_output_dockable.scala"
"src/scala_console.scala"
"src/session_dockable.scala"
+ "src/text_area_painter.scala"
)
declare -a RESOURCES=(
@@ -165,15 +166,29 @@
TARGET="dist/jars/Isabelle-jEdit.jar"
+declare -a UPDATED=()
+
if [ "$BUILD_JARS" = jars_fresh ]; then
OUTDATED=true
else
OUTDATED=false
- for SOURCE in "${SOURCES[@]}" "${RESOURCES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}"
- do
- [ ! -e "$SOURCE" ] && fail "Missing file: $SOURCE"
- [ ! -e "$TARGET" -o "$SOURCE" -nt "$TARGET" ] && OUTDATED=true
- done
+ if [ ! -e "$TARGET" ]; then
+ OUTDATED=true
+ else
+ if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
+ declare -a DEPS=("${SOURCES[@]}" "${RESOURCES[@]}" "$JEDIT_JAR" "${JEDIT_JARS[@]}")
+ else
+ declare -a DEPS=("${SOURCES[@]}" "${RESOURCES[@]}")
+ fi
+ for DEP in "${DEPS[@]}"
+ do
+ [ ! -e "$DEP" ] && fail "Missing file: $DEP"
+ [ "$DEP" -nt "$TARGET" ] && {
+ OUTDATED=true
+ UPDATED["${#UPDATED[@]}"]="$DEP"
+ }
+ done
+ fi
fi
@@ -181,6 +196,14 @@
if [ "$OUTDATED" = true ]
then
+ [ "${#UPDATED[@]}" -gt 0 ] && {
+ echo "Rebuild due to updated file dependencies:"
+ for FILE in "${UPDATED[@]}"
+ do
+ echo " $FILE"
+ done
+ }
+
[ -z "$SCALA_HOME" ] && fail "Unknown SCALA_HOME -- Scala unavailable"
[ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/scriptstyles Wed Jun 15 15:11:18 2011 +0200
@@ -0,0 +1,30 @@
+diff -r jEdit/org/gjt/sp/jedit/syntax/Token.java jEdit-patched/org/gjt/sp/jedit/syntax/Token.java
+60c60
+< return (token == Token.END) ? "END" : TOKEN_TYPES[token];
+---
+> return (token == Token.END) ? "END" : TOKEN_TYPES[(token >= ID_COUNT) ? 0 : token];
+diff -r jEdit/org/gjt/sp/util/SyntaxUtilities.java jEdit-patched/org/gjt/sp/util/SyntaxUtilities.java
+196a197,207
+> * Style with sub/superscript font attribute.
+> */
+> public static SyntaxStyle scriptStyle(String family, int size, int script)
+> {
+> Font font = new Font(family, 0, size);
+> java.util.Map attributes = new java.util.HashMap();
+> attributes.put(java.awt.font.TextAttribute.SUPERSCRIPT, new Integer(script));
+> return new SyntaxStyle(Color.black, null, font.deriveFont(attributes));
+> }
+>
+> /**
+206c217
+< SyntaxStyle[] styles = new SyntaxStyle[Token.ID_COUNT];
+---
+> SyntaxStyle[] styles = new SyntaxStyle[Token.ID_COUNT + 2];
+209c220
+< for(int i = 1; i < styles.length; i++)
+---
+> for(int i = 1; i < Token.ID_COUNT; i++)
+225a237,239
+> styles[Token.ID_COUNT] = scriptStyle(family, size, -1);
+> styles[Token.ID_COUNT + 1] = scriptStyle(family, size, 1);
+>
--- a/src/Tools/jEdit/src/document_model.scala Wed Jun 15 14:36:41 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Wed Jun 15 15:11:18 2011 +0200
@@ -25,36 +25,6 @@
{
object Token_Markup
{
- /* extended token styles */
-
- private val plain_range: Int = Token.ID_COUNT
- private val full_range: Int = 3 * plain_range
- private def check_range(i: Int) { require(0 <= i && i < plain_range) }
-
- def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
- def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
-
- private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
- {
- import scala.collection.JavaConversions._
- val script_font =
- style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
- new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font)
- }
-
- def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
- {
- val new_styles = new Array[SyntaxStyle](full_range)
- for (i <- 0 until plain_range) {
- val style = styles(i)
- new_styles(i) = style
- new_styles(subscript(i.toByte)) = script_style(style, -1)
- new_styles(superscript(i.toByte)) = script_style(style, 1)
- }
- new_styles
- }
-
-
/* line context */
private val dummy_rules = new ParserRuleSet("isabelle", "MAIN")
@@ -197,12 +167,6 @@
val start = buffer.getLineStartOffset(line)
val stop = start + line_segment.count
- /* FIXME
- for (text_area <- Isabelle.jedit_text_areas(buffer)
- if Document_View(text_area).isDefined)
- Document_View(text_area).get.set_styles()
- */
-
def handle_token(style: Byte, offset: Text.Offset, length: Int) =
handler.handleToken(line_segment, style, offset, length, context)
--- a/src/Tools/jEdit/src/document_view.scala Wed Jun 15 14:36:41 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Wed Jun 15 15:11:18 2011 +0200
@@ -17,13 +17,12 @@
FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
import javax.swing.event.{CaretListener, CaretEvent}
-import java.util.ArrayList
import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
import org.gjt.sp.jedit.gui.RolloverButton
import org.gjt.sp.jedit.options.GutterOptionPane
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
-import org.gjt.sp.jedit.syntax.{SyntaxStyle, DisplayTokenHandler, Chunk, Token}
+import org.gjt.sp.jedit.syntax.{SyntaxStyle}
object Document_View
@@ -63,77 +62,13 @@
}
-class Document_View(val model: Document_Model, text_area: JEditTextArea)
+class Document_View(val model: Document_Model, val text_area: JEditTextArea)
{
private val session = model.session
/** token handling **/
- /* extended token styles */
-
- private var styles: Array[SyntaxStyle] = null // owned by Swing thread
-
- def extend_styles()
- {
- Swing_Thread.require()
- styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
- }
- extend_styles()
-
- def set_styles()
- {
- Swing_Thread.require()
- text_area.getPainter.setStyles(styles)
- }
-
-
- /* wrap_margin -- cf. org.gjt.sp.jedit.textarea.TextArea.propertiesChanged */
-
- def wrap_margin(): Int =
- {
- val buffer = text_area.getBuffer
- val painter = text_area.getPainter
- val font = painter.getFont
- val font_context = painter.getFontRenderContext
-
- val soft_wrap = buffer.getStringProperty("wrap") == "soft"
- val max = buffer.getIntegerProperty("maxLineLen", 0)
-
- if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
- else if (soft_wrap)
- painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3
- else 0
- }
-
-
- /* chunks */
-
- def line_chunks(physical_lines: Set[Int]): Map[Text.Offset, Chunk] =
- {
- import scala.collection.JavaConversions._
-
- val buffer = text_area.getBuffer
- val painter = text_area.getPainter
- val margin = wrap_margin().toFloat
-
- val out = new ArrayList[Chunk]
- val handler = new DisplayTokenHandler
-
- var result = Map[Text.Offset, Chunk]()
- for (line <- physical_lines) {
- out.clear
- handler.init(painter.getStyles, painter.getFontRenderContext, painter, out, margin)
- buffer.markTokens(line, handler)
-
- val line_start = buffer.getLineStartOffset(line)
- for (chunk <- handler.getChunkList.iterator)
- result += (line_start + chunk.offset -> chunk)
- }
- result
- }
-
-
/* visible line ranges */
// simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
@@ -209,7 +144,8 @@
}
}
- private var highlight_range: Option[(Text.Range, Color)] = None
+ @volatile private var _highlight_range: Option[(Text.Range, Color)] = None
+ def highlight_range(): Option[(Text.Range, Color)] = _highlight_range
/* CONTROL-mouse management */
@@ -219,12 +155,12 @@
private def exit_control()
{
exit_popup()
- highlight_range = None
+ _highlight_range = None
}
private val focus_listener = new FocusAdapter {
override def focusLost(e: FocusEvent) {
- highlight_range = None // FIXME exit_control !?
+ _highlight_range = None // FIXME exit_control !?
}
}
@@ -246,93 +182,20 @@
if (control) init_popup(snapshot, x, y)
- highlight_range map { case (range, _) => invalidate_line_range(range) }
- highlight_range = if (control) subexp_range(snapshot, x, y) else None
- highlight_range map { case (range, _) => invalidate_line_range(range) }
+ _highlight_range map { case (range, _) => invalidate_line_range(range) }
+ _highlight_range = if (control) subexp_range(snapshot, x, y) else None
+ _highlight_range map { case (range, _) => invalidate_line_range(range) }
}
}
}
- /* TextArea painters */
-
- private val background_painter = new TextAreaExtension
- {
- override def paintScreenLineRange(gfx: Graphics2D,
- first_line: Int, last_line: Int, physical_lines: Array[Int],
- start: Array[Int], end: Array[Int], y: Int, line_height: Int)
- {
- Isabelle.swing_buffer_lock(model.buffer) {
- val snapshot = model.snapshot()
- val ascent = text_area.getPainter.getFontMetrics.getAscent
-
- for (i <- 0 until physical_lines.length) {
- if (physical_lines(i) != -1) {
- val line_range = proper_line_range(start(i), end(i))
-
- // background color: status
- val cmds = snapshot.node.command_range(snapshot.revert(line_range))
- for {
- (command, command_start) <- cmds if !command.is_ignored
- val range = line_range.restrict(snapshot.convert(command.range + command_start))
- r <- Isabelle.gfx_range(text_area, range)
- color <- Isabelle_Markup.status_color(snapshot, command)
- } {
- gfx.setColor(color)
- gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
- }
-
- // background color (1): markup
- for {
- Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
- r <- Isabelle.gfx_range(text_area, range)
- } {
- gfx.setColor(color)
- gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
- }
+ /* text area painting */
- // background color (2): markup
- for {
- Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
- r <- Isabelle.gfx_range(text_area, range)
- } {
- gfx.setColor(color)
- gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
- }
+ private val text_area_painter = new Text_Area_Painter(this)
- // sub-expression highlighting -- potentially from other snapshot
- highlight_range match {
- case Some((range, color)) if line_range.overlaps(range) =>
- Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
- case None =>
- case Some(r) =>
- gfx.setColor(color)
- gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
- }
- case _ =>
- }
-
- // squiggly underline
- for {
- Text.Info(range, Some(color)) <-
- snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
- r <- Isabelle.gfx_range(text_area, range)
- } {
- gfx.setColor(color)
- val x0 = (r.x / 2) * 2
- val y0 = r.y + ascent + 1
- for (x1 <- Range(x0, x0 + r.length, 2)) {
- val y1 = if (x1 % 4 < 2) y0 else y0 + 1
- gfx.drawLine(x1, y1, x1 + 1, y1)
- }
- }
- }
- }
- }
- }
-
+ private val tooltip_painter = new TextAreaExtension
+ {
override def getToolTipText(x: Int, y: Int): String =
{
Isabelle.swing_buffer_lock(model.buffer) {
@@ -357,38 +220,6 @@
}
}
- var use_text_painter = false
-
- private val text_painter = new TextAreaExtension
- {
- override def paintScreenLineRange(gfx: Graphics2D,
- first_line: Int, last_line: Int, physical_lines: Array[Int],
- start: Array[Int], end: Array[Int], y: Int, line_height: Int)
- {
- if (use_text_painter) {
- Isabelle.swing_buffer_lock(model.buffer) {
- val painter = text_area.getPainter
- val fm = painter.getFontMetrics
-
- val all_chunks = line_chunks(Set[Int]() ++ physical_lines.iterator.filter(i => i != -1))
-
- val x0 = text_area.getHorizontalOffset
- var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
- for (i <- 0 until physical_lines.length) {
- if (physical_lines(i) != -1) {
- all_chunks.get(start(i)) match {
- case Some(chunk) =>
- Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR)
- case None =>
- }
- }
- y0 += line_height
- }
- }
- }
- }
- }
-
private val gutter_painter = new TextAreaExtension
{
override def paintScreenLineRange(gfx: Graphics2D,
@@ -557,8 +388,8 @@
private def activate()
{
val painter = text_area.getPainter
- painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
- painter.addExtension(TextAreaPainter.TEXT_LAYER + 1, text_painter)
+ painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
+ text_area_painter.activate()
text_area.getGutter.addExtension(gutter_painter)
text_area.addFocusListener(focus_listener)
text_area.getView.addWindowListener(window_listener)
@@ -580,8 +411,8 @@
text_area.removeCaretListener(caret_listener)
text_area.removeLeftOfScrollBar(overview)
text_area.getGutter.removeExtension(gutter_painter)
- painter.removeExtension(text_painter)
- painter.removeExtension(background_painter)
+ text_area_painter.deactivate()
+ painter.removeExtension(tooltip_painter)
exit_popup()
}
}
--- a/src/Tools/jEdit/src/isabelle_markup.scala Wed Jun 15 14:36:41 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala Wed Jun 15 15:11:18 2011 +0200
@@ -11,6 +11,7 @@
import java.awt.Color
+import org.lobobrowser.util.gui.ColorFactory
import org.gjt.sp.jedit.syntax.Token
@@ -18,6 +19,10 @@
{
/* physical rendering */
+ // see http://www.w3schools.com/css/css_colornames.asp
+
+ def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
+
val outdated_color = new Color(240, 240, 240)
val unfinished_color = new Color(255, 228, 225)
@@ -28,6 +33,9 @@
val bad_color = new Color(255, 106, 106, 100)
val hilite_color = new Color(255, 204, 102, 100)
+ val keyword1_color = get_color("#006699")
+ val keyword2_color = get_color("#009966")
+
class Icon(val priority: Int, val icon: javax.swing.Icon)
{
def >= (that: Icon): Boolean = this.priority >= that.priority
@@ -100,6 +108,35 @@
case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
}
+ private val foreground_colors: Map[String, Color] =
+ Map(
+ Markup.TCLASS -> get_color("red"),
+ Markup.TFREE -> get_color("#A020F0"),
+ Markup.TVAR -> get_color("#A020F0"),
+ Markup.CONST -> get_color("dimgrey"),
+ Markup.FREE -> get_color("blue"),
+ Markup.SKOLEM -> get_color("#D2691E"),
+ Markup.BOUND -> get_color("green"),
+ Markup.VAR -> get_color("#00009B"),
+ Markup.INNER_STRING -> get_color("#D2691E"),
+ Markup.INNER_COMMENT -> get_color("#8B0000"),
+ Markup.DYNAMIC_FACT -> get_color("yellowgreen"),
+ Markup.LITERAL -> keyword1_color,
+ Markup.ML_KEYWORD -> keyword1_color,
+ Markup.ML_DELIMITER -> get_color("black"),
+ Markup.ML_NUMERAL -> get_color("red"),
+ Markup.ML_CHAR -> get_color("#D2691E"),
+ Markup.ML_STRING -> get_color("#D2691E"),
+ Markup.ML_COMMENT -> get_color("#8B0000"),
+ Markup.ML_MALFORMED -> get_color("#FF6A6A")
+ )
+
+ val foreground: Markup_Tree.Select[Color] =
+ {
+ case Text.Info(_, XML.Elem(Markup(m, _), _))
+ if foreground_colors.isDefinedAt(m) => foreground_colors(m)
+ }
+
val tooltip: Markup_Tree.Select[String] =
{
case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\""
@@ -148,40 +185,9 @@
private val token_style: Map[String, Byte] =
{
import Token._
+ val SUBSCRIPT: Byte = ID_COUNT
+ val SUPERSCRIPT: Byte = ID_COUNT + 1
Map[String, Byte](
- // logical entities
- Markup.TCLASS -> NULL,
- Markup.TYCON -> NULL,
- Markup.FIXED -> NULL,
- Markup.CONST -> LITERAL2,
- Markup.DYNAMIC_FACT -> LABEL,
- // inner syntax
- Markup.TFREE -> NULL,
- Markup.FREE -> MARKUP,
- Markup.TVAR -> NULL,
- Markup.SKOLEM -> COMMENT2,
- Markup.BOUND -> LABEL,
- Markup.VAR -> NULL,
- Markup.NUM -> DIGIT,
- Markup.FLOAT -> DIGIT,
- Markup.XNUM -> DIGIT,
- Markup.XSTR -> LITERAL4,
- Markup.LITERAL -> OPERATOR,
- Markup.INNER_COMMENT -> COMMENT1,
- Markup.SORT -> NULL,
- Markup.TYP -> NULL,
- Markup.TERM -> NULL,
- Markup.PROP -> NULL,
- // ML syntax
- Markup.ML_KEYWORD -> KEYWORD1,
- Markup.ML_DELIMITER -> OPERATOR,
- Markup.ML_IDENT -> NULL,
- Markup.ML_TVAR -> NULL,
- Markup.ML_NUMERAL -> DIGIT,
- Markup.ML_CHAR -> LITERAL1,
- Markup.ML_STRING -> LITERAL1,
- Markup.ML_COMMENT -> COMMENT1,
- Markup.ML_MALFORMED -> INVALID,
// embedded source text
Markup.ML_SOURCE -> COMMENT3,
Markup.DOC_SOURCE -> COMMENT3,
--- a/src/Tools/jEdit/src/plugin.scala Wed Jun 15 14:36:41 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Wed Jun 15 15:11:18 2011 +0200
@@ -373,11 +373,7 @@
}
case msg: PropertiesChanged =>
- Swing_Thread.now {
- Isabelle.setup_tooltips()
- for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
- Document_View(text_area).get.extend_styles()
- }
+ Swing_Thread.now { Isabelle.setup_tooltips() }
Isabelle.session.global_settings.event(Session.Global_Settings)
case _ =>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/text_area_painter.scala Wed Jun 15 15:11:18 2011 +0200
@@ -0,0 +1,284 @@
+/* Title: Tools/jEdit/src/text_area_painter.scala
+ Author: Makarius
+
+Painter setup for main jEdit text area.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.Graphics2D
+import java.util.ArrayList
+
+import org.gjt.sp.jedit.Debug
+import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
+import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter}
+
+
+class Text_Area_Painter(doc_view: Document_View)
+{
+ private val model = doc_view.model
+ private val buffer = model.buffer
+ private val text_area = doc_view.text_area
+
+ private val orig_text_painter: TextAreaExtension =
+ {
+ val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText"
+ text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
+ match {
+ case List(x) => x
+ case _ => error("Expected exactly one " + name)
+ }
+ }
+
+
+ /* painter snapshot */
+
+ @volatile private var _painter_snapshot: Option[Document.Snapshot] = None
+
+ private def painter_snapshot(): Document.Snapshot =
+ _painter_snapshot match {
+ case Some(snapshot) => snapshot
+ case None => error("Missing document snapshot for text area painter")
+ }
+
+ private val set_snapshot = new TextAreaExtension
+ {
+ override def paintScreenLineRange(gfx: Graphics2D,
+ first_line: Int, last_line: Int, physical_lines: Array[Int],
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ {
+ _painter_snapshot = Some(model.snapshot())
+ }
+ }
+
+ private val reset_snapshot = new TextAreaExtension
+ {
+ override def paintScreenLineRange(gfx: Graphics2D,
+ first_line: Int, last_line: Int, physical_lines: Array[Int],
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ {
+ _painter_snapshot = None
+ }
+ }
+
+
+ /* text background */
+
+ private val background_painter = new TextAreaExtension
+ {
+ override def paintScreenLineRange(gfx: Graphics2D,
+ first_line: Int, last_line: Int, physical_lines: Array[Int],
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ {
+ Isabelle.swing_buffer_lock(buffer) {
+ val snapshot = painter_snapshot()
+ val ascent = text_area.getPainter.getFontMetrics.getAscent
+
+ for (i <- 0 until physical_lines.length) {
+ if (physical_lines(i) != -1) {
+ val line_range = doc_view.proper_line_range(start(i), end(i))
+
+ // background color: status
+ val cmds = snapshot.node.command_range(snapshot.revert(line_range))
+ for {
+ (command, command_start) <- cmds if !command.is_ignored
+ val range = line_range.restrict(snapshot.convert(command.range + command_start))
+ r <- Isabelle.gfx_range(text_area, range)
+ color <- Isabelle_Markup.status_color(snapshot, command)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+ }
+
+ // background color (1): markup
+ for {
+ Text.Info(range, Some(color)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
+ r <- Isabelle.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+ }
+
+ // background color (2): markup
+ for {
+ Text.Info(range, Some(color)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
+ r <- Isabelle.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
+ }
+
+ // sub-expression highlighting -- potentially from other snapshot
+ doc_view.highlight_range match {
+ case Some((range, color)) if line_range.overlaps(range) =>
+ Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
+ case None =>
+ case Some(r) =>
+ gfx.setColor(color)
+ gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
+ }
+ case _ =>
+ }
+
+ // squiggly underline
+ for {
+ Text.Info(range, Some(color)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
+ r <- Isabelle.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ val x0 = (r.x / 2) * 2
+ val y0 = r.y + ascent + 1
+ for (x1 <- Range(x0, x0 + r.length, 2)) {
+ val y1 = if (x1 % 4 < 2) y0 else y0 + 1
+ gfx.drawLine(x1, y1, x1 + 1, y1)
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+
+
+ /* text */
+
+ private def line_infos(physical_lines: Iterator[Int]): Map[Text.Offset, Chunk] =
+ {
+ val painter = text_area.getPainter
+ val font = painter.getFont
+ val font_context = painter.getFontRenderContext
+
+ // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
+ // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
+ val margin =
+ if (buffer.getStringProperty("wrap") != "soft") 0.0f
+ else {
+ val max = buffer.getIntegerProperty("maxLineLen", 0)
+ if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
+ else painter.getWidth - font.getStringBounds(" ", font_context).getWidth.round.toInt * 3
+ }.toFloat
+
+ val out = new ArrayList[Chunk]
+ val handler = new DisplayTokenHandler
+
+ var result = Map[Text.Offset, Chunk]()
+ for (line <- physical_lines) {
+ out.clear
+ handler.init(painter.getStyles, font_context, painter, out, margin)
+ buffer.markTokens(line, handler)
+
+ val line_start = buffer.getLineStartOffset(line)
+ for (i <- 0 until out.size) {
+ val chunk = out.get(i)
+ result += (line_start + chunk.offset -> chunk)
+ }
+ }
+ result
+ }
+
+ private def paint_chunk_list(gfx: Graphics2D,
+ offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
+ {
+ val clip_rect = gfx.getClipBounds
+ val font_context = text_area.getPainter.getFontRenderContext
+
+ var w = 0.0f
+ var chunk_offset = offset
+ var chunk = head
+ while (chunk != null) {
+ val chunk_length = if (chunk.str == null) 0 else chunk.str.length
+
+ if (x + w + chunk.width > clip_rect.x &&
+ x + w < clip_rect.x + clip_rect.width &&
+ chunk.accessable && chunk.visible)
+ {
+ val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk_length)
+ val chunk_font = chunk.style.getFont
+ val chunk_color = chunk.style.getForegroundColor
+
+ val markup = painter_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
+
+ gfx.setFont(chunk_font)
+ if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
+ markup.forall(info => info.info.isEmpty)) {
+ gfx.setColor(chunk_color)
+ gfx.drawGlyphVector(chunk.gv, x + w, y)
+ }
+ else {
+ var x1 = x + w
+ for (Text.Info(range, info) <- markup) {
+ val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
+ gfx.setColor(info.getOrElse(chunk_color))
+ gfx.drawString(str, x1.toInt, y.toInt)
+ x1 += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
+ }
+ }
+ }
+ w += chunk.width
+ chunk_offset += chunk_length
+ chunk = chunk.next.asInstanceOf[Chunk]
+ }
+ w
+ }
+
+ private val text_painter = new TextAreaExtension
+ {
+ override def paintScreenLineRange(gfx: Graphics2D,
+ first_line: Int, last_line: Int, physical_lines: Array[Int],
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ {
+ Isabelle.swing_buffer_lock(buffer) {
+ val clip = gfx.getClip
+ val x0 = text_area.getHorizontalOffset
+ val fm = text_area.getPainter.getFontMetrics
+ var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
+
+ val infos = line_infos(physical_lines.iterator.filter(i => i != -1))
+ for (i <- 0 until physical_lines.length) {
+ if (physical_lines(i) != -1) {
+ infos.get(start(i)) match {
+ case Some(chunk) =>
+ val w = paint_chunk_list(gfx, start(i), chunk, x0, y0).toInt
+ gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
+ orig_text_painter.paintValidLine(gfx,
+ first_line + i, physical_lines(i), start(i), end(i), y + line_height * i)
+ gfx.setClip(clip)
+ case None =>
+ }
+ }
+ y0 += line_height
+ }
+ }
+ }
+ }
+
+
+ /* activation */
+
+ def activate()
+ {
+ val painter = text_area.getPainter
+ painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot)
+ painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
+ painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
+ painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
+ painter.removeExtension(orig_text_painter)
+ }
+
+ def deactivate()
+ {
+ val painter = text_area.getPainter
+ painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
+ painter.removeExtension(reset_snapshot)
+ painter.removeExtension(text_painter)
+ painter.removeExtension(background_painter)
+ painter.removeExtension(set_snapshot)
+ }
+}
+