--- a/Admin/CHECKLIST Sat Sep 10 19:44:41 2011 +0200
+++ b/Admin/CHECKLIST Sat Sep 10 20:41:27 2011 +0200
@@ -11,6 +11,8 @@
- check persistent sessions with PG and Poly/ML 5.x;
+- check file positions within logic images (hyperlinks etc.);
+
- Admin/update-keywords;
- check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
--- a/Isabelle Sat Sep 10 19:44:41 2011 +0200
+++ b/Isabelle Sat Sep 10 20:41:27 2011 +0200
@@ -2,27 +2,7 @@
#
# Author: Makarius
#
-# Generic Isabelle application wrapper.
-
-if [ -L "$0" ]; then
- TARGET="$(LC_ALL=C ls -l "$0" | sed 's/.* -> //')"
- exec "$(cd "$(dirname "$0")"; cd "$(pwd -P)"; cd "$(dirname "$TARGET")"; pwd)/$(basename "$TARGET")" "$@"
-fi
-
-
-## settings
+# Default Isabelle application wrapper.
-ISABELLE_HOME="$(cd "$(dirname "$0")"; pwd -P)"
-source "$ISABELLE_HOME/lib/scripts/getsettings" || exit 2
-
-unset ISABELLE_SETTINGS_PRESENT
-unset ISABELLE_SITE_SETTINGS_PRESENT
-
+exec "$(dirname "$0")"/bin/isabelle jedit "$@"
-## main
-
-[ -e "$ISABELLE_HOME/Admin/build" ] && "$ISABELLE_HOME/Admin/build" jars
-
-exec "$ISABELLE_TOOL" java \
- "-Disabelle.home=$(jvmpath "$ISABELLE_HOME")" \
- isabelle.GUI_Setup "$@"
--- a/src/Pure/General/path.ML Sat Sep 10 19:44:41 2011 +0200
+++ b/src/Pure/General/path.ML Sat Sep 10 20:41:27 2011 +0200
@@ -185,9 +185,20 @@
val expand = rep #> maps eval #> norm #> Path;
-(* source position *)
+(* source position -- with smart replacement ISABELLE_HOME *)
+
+val isabelle_home = explode_path "~~";
-val position = Position.file o implode_path o expand;
+fun position path =
+ let
+ val s = implode_path path;
+ val prfx = implode_path (expand isabelle_home) ^ "/";
+ in
+ Position.file
+ (case try (unprefix prfx) s of
+ NONE => s
+ | SOME s' => "~~/" ^ s')
+ end;
(*final declarations of this structure!*)
--- a/src/Pure/PIDE/isar_document.scala Sat Sep 10 19:44:41 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala Sat Sep 10 20:41:27 2011 +0200
@@ -63,6 +63,9 @@
}
sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
+ {
+ def total: Int = unprocessed + running + finished + failed
+ }
def node_status(
state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
--- a/src/Tools/jEdit/lib/Tools/jedit Sat Sep 10 19:44:41 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Sat Sep 10 20:41:27 2011 +0200
@@ -57,6 +57,7 @@
echo " -m MODE add print mode for output"
echo
echo "Start jEdit with Isabelle plugin setup and opens theory FILES"
+ echo "(default Scratch.thy)."
echo
exit 1
}
--- a/src/Tools/jEdit/src/Isabelle.props Sat Sep 10 19:44:41 2011 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Sat Sep 10 20:41:27 2011 +0200
@@ -38,8 +38,15 @@
options.isabelle.auto-start=true
#actions
+isabelle.check-buffer.label=Commence full proof checking of current buffer
+isabelle.check-buffer.shortcut=C+e SPACE
+isabelle.cancel-execution.label=Cancel current proof checking process
+isabelle.cancel-execution.shortcut=C+e BACK_SPACE
+isabelle.input-isub.label=Input subscript
isabelle.input-isub.shortcut=C+e DOWN
+isabelle.input-isup.label=Input superscript
isabelle.input-isup.shortcut=C+e UP
+isabelle.input-bold.label=Input bold face
isabelle.input-bold.shortcut=C+e RIGHT
#menu actions
--- a/src/Tools/jEdit/src/actions.xml Sat Sep 10 19:44:41 2011 +0200
+++ b/src/Tools/jEdit/src/actions.xml Sat Sep 10 20:41:27 2011 +0200
@@ -57,5 +57,14 @@
isabelle.jedit.Isabelle.input_bold(textArea);
</CODE>
</ACTION>
-
+ <ACTION NAME="isabelle.check-buffer">
+ <CODE>
+ isabelle.jedit.Isabelle.check_buffer(buffer);
+ </CODE>
+ </ACTION>
+ <ACTION NAME="isabelle.cancel-execution">
+ <CODE>
+ isabelle.jedit.Isabelle.cancel_execution();
+ </CODE>
+ </ACTION>
</ACTIONS>
\ No newline at end of file
--- a/src/Tools/jEdit/src/isabelle_markup.scala Sat Sep 10 19:44:41 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala Sat Sep 10 20:41:27 2011 +0200
@@ -26,13 +26,14 @@
val outdated_color = new Color(238, 227, 227)
val running_color = new Color(97, 0, 97)
val running1_color = new Color(97, 0, 97, 100)
- val unfinished_color = new Color(255, 160, 160)
- val unfinished1_color = new Color(255, 160, 160, 50)
+ val unprocessed_color = new Color(255, 160, 160)
+ val unprocessed1_color = new Color(255, 160, 160, 50)
val light_color = new Color(240, 240, 240)
val regular_color = new Color(192, 192, 192)
val warning_color = new Color(255, 140, 0)
val error_color = new Color(178, 34, 34)
+ val error1_color = new Color(178, 34, 34, 50)
val bad_color = new Color(255, 106, 106, 100)
val hilite_color = new Color(255, 204, 102, 100)
@@ -60,7 +61,7 @@
else
Isar_Document.command_status(state.status) match {
case Isar_Document.Forked(i) if i > 0 => Some(running1_color)
- case Isar_Document.Unprocessed => Some(unfinished1_color)
+ case Isar_Document.Unprocessed => Some(unprocessed1_color)
case _ => None
}
}
@@ -72,7 +73,7 @@
else
Isar_Document.command_status(state.status) match {
case Isar_Document.Forked(i) => if (i > 0) Some(running_color) else None
- case Isar_Document.Unprocessed => Some(unfinished_color)
+ case Isar_Document.Unprocessed => Some(unprocessed_color)
case Isar_Document.Failed => Some(error_color)
case Isar_Document.Finished =>
if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
--- a/src/Tools/jEdit/src/plugin.scala Sat Sep 10 19:44:41 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Sat Sep 10 20:41:27 2011 +0200
@@ -343,6 +343,16 @@
def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)
def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)
def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded)
+
+ def check_buffer(buffer: Buffer)
+ {
+ document_model(buffer) match {
+ case None =>
+ case Some(model) => model.full_perspective()
+ }
+ }
+
+ def cancel_execution() { session.cancel_execution() }
}
--- a/src/Tools/jEdit/src/session_dockable.scala Sat Sep 10 19:44:41 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala Sat Sep 10 20:41:27 2011 +0200
@@ -15,11 +15,11 @@
import scala.swing.event.{ButtonClicked, SelectionChanged}
import java.lang.System
-import java.awt.BorderLayout
-import javax.swing.JList
+import java.awt.{BorderLayout, Graphics}
+import javax.swing.{JList, DefaultListCellRenderer}
import javax.swing.border.{BevelBorder, SoftBevelBorder}
-import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.{View, jEdit}
class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
@@ -62,21 +62,14 @@
session_phase.tooltip = "Prover status"
private val cancel = new Button("Cancel") {
- reactions += { case ButtonClicked(_) => Isabelle.session.cancel_execution }
+ reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() }
}
- cancel.tooltip = "Cancel current proof checking process"
+ cancel.tooltip = jEdit.getProperty("isabelle.cancel-execution.label")
private val check = new Button("Check") {
- reactions +=
- {
- case ButtonClicked(_) =>
- Isabelle.document_model(view.getBuffer) match {
- case None =>
- case Some(model) => model.full_perspective()
- }
- }
+ reactions += { case ButtonClicked(_) => Isabelle.check_buffer(view.getBuffer) }
}
- check.tooltip = "Commence full proof checking of current buffer"
+ check.tooltip = jEdit.getProperty("isabelle.check-buffer.label")
private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
logic.listenTo(logic.selection)
@@ -91,7 +84,35 @@
/* component state -- owned by Swing thread */
- private var nodes_status: Map[Document.Node.Name, String] = Map.empty
+ private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty
+
+ val node_renderer = new DefaultListCellRenderer
+ {
+ override def paintComponent(gfx: Graphics)
+ {
+ nodes_status.get(Document.Node.Name(getText, "", "")) match {
+ case Some(st) if st.total > 0 =>
+ val w = getWidth
+ val h = getHeight
+ var end = w
+ for {
+ (n, color) <- List(
+ (st.unprocessed, Isabelle_Markup.unprocessed1_color),
+ (st.running, Isabelle_Markup.running_color),
+ (st.failed, Isabelle_Markup.error_color)) }
+ {
+ gfx.setColor(color)
+ val v = (n * w / st.total) max (if (n > 0) 2 else 0)
+ gfx.fillRect(end - v, 0, v, h)
+ end -= v
+ }
+ case _ =>
+ }
+ super.paintComponent(gfx)
+ }
+ }
+
+ status.peer.setCellRenderer(node_renderer)
private def handle_changed(changed_nodes: Set[Document.Node.Name])
{
@@ -105,14 +126,13 @@
name <- changed_nodes
node <- version.nodes.get(name)
val status = Isar_Document.node_status(state, version, node)
- } nodes_status1 += (name -> status.toString)
+ } nodes_status1 += (name -> status)
if (nodes_status != nodes_status1) {
nodes_status = nodes_status1
- val order =
- Library.sort_wrt((name: Document.Node.Name) => name.theory,
- nodes_status.keySet.toList)
- status.listData = order.map(name => name.theory + " " + nodes_status(name))
+ status.listData =
+ Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
+ .map(_.node)
}
}
}