# HG changeset patch # User wenzelm # Date 1334870327 -7200 # Node ID f5eaa7fa8d7285e6794515dc23a80b9c59aeb623 # Parent 632a1e5710e6842fc4e6404ff80683826b15e230# Parent 0ddac15782e4d1f207e3f29f64707944a3dff100 merged diff -r 632a1e5710e6 -r f5eaa7fa8d72 Admin/isatest/settings/at-poly --- 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" diff -r 632a1e5710e6 -r f5eaa7fa8d72 Admin/isatest/settings/at-poly-e --- 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" diff -r 632a1e5710e6 -r f5eaa7fa8d72 Admin/isatest/settings/at-poly-test --- 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" diff -r 632a1e5710e6 -r f5eaa7fa8d72 Admin/isatest/settings/at64-poly --- 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" diff -r 632a1e5710e6 -r f5eaa7fa8d72 Admin/isatest/settings/cygwin-poly-e --- 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" diff -r 632a1e5710e6 -r f5eaa7fa8d72 NEWS --- 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 diff -r 632a1e5710e6 -r f5eaa7fa8d72 doc-src/IsarRef/style.sty --- 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}} diff -r 632a1e5710e6 -r f5eaa7fa8d72 src/Tools/jEdit/src/isabelle_sidekick.scala --- 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 + } + } + */ + } } } } diff -r 632a1e5710e6 -r f5eaa7fa8d72 src/Tools/jEdit/src/jEdit.props --- 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 diff -r 632a1e5710e6 -r f5eaa7fa8d72 src/Tools/jEdit/src/output_dockable.scala --- 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 => diff -r 632a1e5710e6 -r f5eaa7fa8d72 src/Tools/jEdit/src/session_dockable.scala --- 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}