# HG changeset patch # User blanchet # Date 1308143478 -7200 # Node ID b35ff420d72094399f9ce14ecfc0306da23fc20a # Parent e93dfcb53535b8a59d7d7ffa39c6a9cdd0b98fc9# Parent 7ee98a3802af513cc7a01fabe6878949672c54bd merge diff -r e93dfcb53535 -r b35ff420d720 Admin/isatest/isatest-makedist --- 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" diff -r e93dfcb53535 -r b35ff420d720 Admin/isatest/settings/at-poly-test --- 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" diff -r e93dfcb53535 -r b35ff420d720 doc-src/IsarRef/Thy/Generic.thy --- 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 "\ 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 \ - 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 "\ 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 \ 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} *} diff -r e93dfcb53535 -r b35ff420d720 doc-src/IsarRef/Thy/document/Generic.tex --- 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}% diff -r e93dfcb53535 -r b35ff420d720 doc-src/Ref/classical.tex --- 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} diff -r e93dfcb53535 -r b35ff420d720 src/HOL/Library/Executable_Set.thy --- 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] diff -r e93dfcb53535 -r b35ff420d720 src/HOL/Mutabelle/lib/Tools/mutabelle --- 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 *) ] *} diff -r e93dfcb53535 -r b35ff420d720 src/HOL/Quickcheck_Narrowing.thy --- 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" diff -r e93dfcb53535 -r b35ff420d720 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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; diff -r e93dfcb53535 -r b35ff420d720 src/HOL/Tools/SMT/smt_datatypes.ML --- 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 diff -r e93dfcb53535 -r b35ff420d720 src/HOL/Tools/SMT/smt_translate.ML --- 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 diff -r e93dfcb53535 -r b35ff420d720 src/Pure/General/markup.scala --- 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" diff -r e93dfcb53535 -r b35ff420d720 src/Tools/jEdit/lib/Tools/jedit --- 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" ] && \ diff -r e93dfcb53535 -r b35ff420d720 src/Tools/jEdit/patches/scriptstyles --- /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); +> diff -r e93dfcb53535 -r b35ff420d720 src/Tools/jEdit/src/document_model.scala --- 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) diff -r e93dfcb53535 -r b35ff420d720 src/Tools/jEdit/src/document_view.scala --- 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() } } diff -r e93dfcb53535 -r b35ff420d720 src/Tools/jEdit/src/isabelle_markup.scala --- 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, diff -r e93dfcb53535 -r b35ff420d720 src/Tools/jEdit/src/plugin.scala --- 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 _ => diff -r e93dfcb53535 -r b35ff420d720 src/Tools/jEdit/src/text_area_painter.scala --- /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) + } +} +