--- a/Admin/isatest/settings/at-poly Thu Apr 19 22:21:15 2012 +0200
+++ b/Admin/isatest/settings/at-poly Thu Apr 19 23:18:47 2012 +0200
@@ -24,5 +24,6 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true"
+init_component "$HOME/contrib_devel/jdk-7u3_x86-linux"
init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/Admin/isatest/settings/at-poly-e Thu Apr 19 22:21:15 2012 +0200
+++ b/Admin/isatest/settings/at-poly-e Thu Apr 19 23:18:47 2012 +0200
@@ -24,4 +24,5 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true -t true"
+init_component "$HOME/contrib_devel/jdk-7u3_x86-linux"
init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/Admin/isatest/settings/at-poly-test Thu Apr 19 22:21:15 2012 +0200
+++ b/Admin/isatest/settings/at-poly-test Thu Apr 19 23:18:47 2012 +0200
@@ -28,4 +28,5 @@
ISABELLE_OCAML="/home/isabelle/contrib_devel/ocaml/x86-linux/ocaml"
ISABELLE_SWIPL="/home/isabelle/contrib_devel/swipl/bin/swipl"
+init_component "$HOME/contrib_devel/jdk-7u3_x86-linux"
init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/Admin/isatest/settings/at64-poly Thu Apr 19 22:21:15 2012 +0200
+++ b/Admin/isatest/settings/at64-poly Thu Apr 19 23:18:47 2012 +0200
@@ -24,4 +24,5 @@
ISABELLE_USEDIR_OPTIONS="-i true -d pdf -v true"
+init_component "$HOME/contrib_devel/jdk-7u3_x86_64-linux"
init_component "$HOME/contrib_devel/kodkodi-1.2.16"
--- a/Admin/isatest/settings/cygwin-poly-e Thu Apr 19 22:21:15 2012 +0200
+++ b/Admin/isatest/settings/cygwin-poly-e Thu Apr 19 23:18:47 2012 +0200
@@ -24,4 +24,5 @@
ISABELLE_USEDIR_OPTIONS="-M 1 -i false -d false"
+init_component "$HOME/contrib_devel/jdk-7u3_x86-linux"
init_component "$HOME/contrib/kodkodi-1.2.16"
--- a/NEWS Thu Apr 19 22:21:15 2012 +0200
+++ b/NEWS Thu Apr 19 23:18:47 2012 +0200
@@ -8,6 +8,8 @@
* Prover IDE (PIDE) improvements:
+ - more robust Sledgehammer integration (as before the sledgehammer
+ command line needs to be typed into the source buffer)
- markup for bound variables
- markup for types of term variables (e.g. displayed as tooltips)
- support for user-defined Isar commands within the running session
--- a/doc-src/IsarRef/style.sty Thu Apr 19 22:21:15 2012 +0200
+++ b/doc-src/IsarRef/style.sty Thu Apr 19 23:18:47 2012 +0200
@@ -13,16 +13,18 @@
\newcommand{\figref}[1]{figure~\ref{#1}}
\newcommand{\Figref}[1]{Figure~\ref{#1}}
+%% Isar
+\newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
+\isafoldtag{noproof}\def\isafoldnoproof{~\isafold{proof}}
+\newcommand{\isadigitreset}{\def\isadigit##1{##1}}
+\renewcommand{\isacommand}[1]{\isakeyword{\isadigitreset#1}}
+
%% ML
\newenvironment{mldecls}{\par\noindent\begingroup\def\isanewline{\\}\begin{tabular}{ll}}{\end{tabular}\medskip\endgroup}
-\renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\def\isadigit##1{##1}}
+\renewcommand{\isatagML}{\begingroup\isabellestyle{default}\isastyle\isadigitreset}
\renewcommand{\endisatagML}{\endgroup}
-%% Isar
-\newcommand{\isasymBBAR}{{\,\newdimen{\tmpheight}\settoheight\tmpheight{\isacharbar}\rule{1pt}{\tmpheight}\,}}
-\isafoldtag{noproof}\def\isafoldnoproof{~\isafold{proof}}
-
%% math
\newcommand{\isasymstrut}{\isamath{\mathstrut}}
\newcommand{\isasymvartheta}{\isamath{\,\theta}}
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Apr 19 22:21:15 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Apr 19 23:18:47 2012 +0200
@@ -13,13 +13,15 @@
import scala.collection.Set
import scala.collection.immutable.TreeSet
+import java.awt.Component
import javax.swing.tree.DefaultMutableTreeNode
import javax.swing.text.Position
-import javax.swing.Icon
+import javax.swing.{Icon, DefaultListCellRenderer, ListCellRenderer, JList}
import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
import errorlist.DefaultErrorSource
-import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
+import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion,
+ SideKickCompletionPopup, IAsset}
object Isabelle_Sidekick
@@ -101,8 +103,27 @@
cs.map(Symbol.decode(_)).sorted
else cs).filter(_ != word)
if (ds.isEmpty) null
- else new SideKickCompletion(
- pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
+ else
+ new SideKickCompletion(pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) {
+ /* FIXME Java 7 only
+ override def getRenderer() =
+ new ListCellRenderer[Any] {
+ val default_renderer =
+ (new DefaultListCellRenderer).asInstanceOf[ListCellRenderer[Any]]
+
+ override def getListCellRendererComponent(
+ list: JList[_ <: Any], value: Any, index: Int,
+ selected: Boolean, focus: Boolean): Component =
+ {
+ val renderer: Component =
+ default_renderer.getListCellRendererComponent(
+ list, value, index, selected, focus)
+ renderer.setFont(pane.getTextArea.getPainter.getFont)
+ renderer
+ }
+ }
+ */
+ }
}
}
}
--- a/src/Tools/jEdit/src/jEdit.props Thu Apr 19 22:21:15 2012 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Thu Apr 19 23:18:47 2012 +0200
@@ -191,8 +191,12 @@
restore.remote=false
restore=false
sidekick-tree.dock-position=right
+sidekick.auto-complete-popup-get-focus=true
sidekick.buffer-save-parse=true
sidekick.complete-delay=300
+sidekick.complete-instant.toggle=false
+sidekick.complete-popup.accept-characters=\\n\\t
+sidekick.complete-popup.insert-characters=
sidekick.splitter.location=721
tip.show=false
twoStageSave=false
--- a/src/Tools/jEdit/src/output_dockable.scala Thu Apr 19 22:21:15 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Thu Apr 19 23:18:47 2012 +0200
@@ -44,10 +44,12 @@
snapshot.node.command_start(cmd) match {
case Some(start) if !snapshot.is_outdated =>
val text = Pretty.string_of(sendback)
- buffer.beginCompoundEdit()
- buffer.remove(start, cmd.proper_range.length)
- buffer.insert(start, text)
- buffer.endCompoundEdit()
+ try {
+ buffer.beginCompoundEdit()
+ buffer.remove(start, cmd.proper_range.length)
+ buffer.insert(start, text)
+ }
+ finally { buffer.endCompoundEdit() }
case _ =>
}
case None =>
--- a/src/Tools/jEdit/src/session_dockable.scala Thu Apr 19 22:21:15 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala Thu Apr 19 23:18:47 2012 +0200
@@ -16,7 +16,7 @@
import java.lang.System
import java.awt.{BorderLayout, Graphics2D, Insets}
-import javax.swing.{JList, DefaultListCellRenderer, BorderFactory}
+import javax.swing.{JList, BorderFactory}
import javax.swing.border.{BevelBorder, SoftBevelBorder}
import org.gjt.sp.jedit.{View, jEdit}