# HG changeset patch # User wenzelm # Date 1354307424 -3600 # Node ID f70b3712040fece5bb797cfd58c5f6e74c39453d # Parent 1426d478ccda46319c5a2098c293f043eea040c0 renamed dockable "Prover Session" to "Theories"; more uniform Library.lowercase/uppercase; diff -r 1426d478ccda -r f70b3712040f src/Pure/System/options.scala --- a/src/Pure/System/options.scala Fri Nov 30 21:28:35 2012 +0100 +++ b/src/Pure/System/options.scala Fri Nov 30 21:30:24 2012 +0100 @@ -7,7 +7,6 @@ package isabelle -import java.util.Locale import java.util.Calendar @@ -22,7 +21,7 @@ sealed abstract class Type { - def print: String = toString.toLowerCase(Locale.ENGLISH) + def print: String = Library.lowercase(toString) } case object Bool extends Type case object Int extends Type diff -r 1426d478ccda -r f70b3712040f src/Pure/System/standard_system.scala --- a/src/Pure/System/standard_system.scala Fri Nov 30 21:28:35 2012 +0100 +++ b/src/Pure/System/standard_system.scala Fri Nov 30 21:30:24 2012 +0100 @@ -9,7 +9,6 @@ import java.lang.System import java.util.regex.Pattern -import java.util.Locale import java.net.URL import java.io.{File => JFile} @@ -94,7 +93,7 @@ val rest = posix_path match { case Cygdrive(drive, rest) => - result_path ++= (drive.toUpperCase(Locale.ENGLISH) + ":" + JFile.separator) + result_path ++= (Library.uppercase(drive) + ":" + JFile.separator) rest case Named_Root(root, rest) => result_path ++= JFile.separator @@ -129,7 +128,7 @@ jvm_path.replace('/', '\\') match { case Platform_Root(rest) => "/" + rest.replace('\\', '/') case Drive(letter, rest) => - "/cygdrive/" + letter.toLowerCase(Locale.ENGLISH) + + "/cygdrive/" + Library.lowercase(letter) + (if (rest == "") "" else "/" + rest.replace('\\', '/')) case path => path.replace('\\', '/') } diff -r 1426d478ccda -r f70b3712040f src/Pure/library.scala --- a/src/Pure/library.scala Fri Nov 30 21:28:35 2012 +0100 +++ b/src/Pure/library.scala Fri Nov 30 21:30:24 2012 +0100 @@ -85,9 +85,12 @@ if (str.endsWith("\n")) str.substring(0, str.length - 1) else str + def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH) + def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH) + def capitalize(str: String): String = if (str.length == 0) str - else str.substring(0, 1).toUpperCase(Locale.ENGLISH) + str.substring(1) + else uppercase(str.substring(0, 1)) + str.substring(1) /* quote */ diff -r 1426d478ccda -r f70b3712040f src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Fri Nov 30 21:28:35 2012 +0100 +++ b/src/Tools/jEdit/lib/Tools/jedit Fri Nov 30 21:30:24 2012 +0100 @@ -35,10 +35,10 @@ "src/rich_text_area.scala" "src/scala_console.scala" "src/sendback.scala" - "src/session_dockable.scala" "src/symbols_dockable.scala" "src/syslog_dockable.scala" "src/text_overview.scala" + "src/theories_dockable.scala" "src/token_markup.scala" ) diff -r 1426d478ccda -r f70b3712040f src/Tools/jEdit/src/Isabelle.props --- a/src/Tools/jEdit/src/Isabelle.props Fri Nov 30 21:28:35 2012 +0100 +++ b/src/Tools/jEdit/src/Isabelle.props Fri Nov 30 21:30:24 2012 +0100 @@ -47,8 +47,8 @@ #menu actions plugin.isabelle.jedit.Plugin.menu.label=Isabelle -plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.graphview-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.symbols-panel isabelle.syslog-panel -isabelle.session-panel.label=Prover Session panel +plugin.isabelle.jedit.Plugin.menu=isabelle.theories-panel isabelle.output-panel isabelle.graphview-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.symbols-panel isabelle.syslog-panel +isabelle.theories-panel.label=Theories panel isabelle.output-panel.label=Output panel isabelle.graphview-panel.label=Graphview panel isabelle.raw-output-panel.label=Raw Output panel @@ -58,7 +58,7 @@ isabelle.syslog-panel.label=Syslog panel #dockables -isabelle-session.title=Prover Session +isabelle-theories.title=Theories isabelle-output.title=Output isabelle-info.title=Info isabelle-graphview.title=Graphview diff -r 1426d478ccda -r f70b3712040f src/Tools/jEdit/src/actions.xml --- a/src/Tools/jEdit/src/actions.xml Fri Nov 30 21:28:35 2012 +0100 +++ b/src/Tools/jEdit/src/actions.xml Fri Nov 30 21:30:24 2012 +0100 @@ -2,9 +2,9 @@ - + - wm.addDockableWindow("isabelle-session"); + wm.addDockableWindow("isabelle-theories"); diff -r 1426d478ccda -r f70b3712040f src/Tools/jEdit/src/dockables.xml --- a/src/Tools/jEdit/src/dockables.xml Fri Nov 30 21:28:35 2012 +0100 +++ b/src/Tools/jEdit/src/dockables.xml Fri Nov 30 21:30:24 2012 +0100 @@ -2,8 +2,8 @@ - - new isabelle.jedit.Session_Dockable(view, position); + + new isabelle.jedit.Theories_Dockable(view, position); new isabelle.jedit.Syslog_Dockable(view, position); diff -r 1426d478ccda -r f70b3712040f src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Fri Nov 30 21:28:35 2012 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Fri Nov 30 21:30:24 2012 +0100 @@ -20,9 +20,9 @@ private def wm(view: View): DockableWindowManager = view.getDockableWindowManager - def docked_session(view: View): Option[Session_Dockable] = - wm(view).getDockableWindow("isabelle-session") match { - case dockable: Session_Dockable => Some(dockable) + def docked_theories(view: View): Option[Theories_Dockable] = + wm(view).getDockableWindow("isabelle-theories") match { + case dockable: Theories_Dockable => Some(dockable) case _ => None } diff -r 1426d478ccda -r f70b3712040f src/Tools/jEdit/src/jEdit.props --- a/src/Tools/jEdit/src/jEdit.props Fri Nov 30 21:28:35 2012 +0100 +++ b/src/Tools/jEdit/src/jEdit.props Fri Nov 30 21:30:24 2012 +0100 @@ -181,7 +181,7 @@ isabelle-output.height=174 isabelle-output.width=412 isabelle-readme.dock-position=bottom -isabelle-session.dock-position=bottom +isabelle-theories.dock-position=bottom isabelle-symbols.dock-position=bottom line-end.shortcut=END line-home.shortcut=HOME diff -r 1426d478ccda -r f70b3712040f src/Tools/jEdit/src/session_dockable.scala --- a/src/Tools/jEdit/src/session_dockable.scala Fri Nov 30 21:28:35 2012 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,176 +0,0 @@ -/* Title: Tools/jEdit/src/session_dockable.scala - Author: Makarius - -Dockable window for prover session management. -*/ - -package isabelle.jedit - - -import isabelle._ - -import scala.actors.Actor._ -import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component} -import scala.swing.event.{ButtonClicked, MouseClicked} - -import java.lang.System -import java.awt.{BorderLayout, Graphics2D, Insets} -import javax.swing.{JList, BorderFactory} -import javax.swing.border.{BevelBorder, SoftBevelBorder} - -import org.gjt.sp.jedit.{View, jEdit} - - -class Session_Dockable(view: View, position: String) extends Dockable(view, position) -{ - /* status */ - - private val status = new ListView(Nil: List[Document.Node.Name]) { - listenTo(mouse.clicks) - reactions += { - case MouseClicked(_, point, _, clicks, _) if clicks == 2 => - val index = peer.locationToIndex(point) - if (index >= 0) jEdit.openFile(view, listData(index).node) - } - } - status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP) - status.peer.setVisibleRowCount(0) - status.selection.intervalMode = ListView.IntervalMode.Single - - set_content(new ScrollPane(status)) - - - /* controls */ - - private val session_phase = new Label(PIDE.session.phase.toString) - session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED) - session_phase.tooltip = "Prover status" - - private def handle_phase(phase: Session.Phase) - { - Swing_Thread.later { session_phase.text = " " + phase.toString + " " } - } - - private val cancel = new Button("Cancel") { - reactions += { case ButtonClicked(_) => PIDE.cancel_execution() } - } - cancel.tooltip = jEdit.getProperty("isabelle.cancel-execution.label") - - private val check = new Button("Check") { - reactions += { case ButtonClicked(_) => PIDE.check_buffer(view.getBuffer) } - } - check.tooltip = jEdit.getProperty("isabelle.check-buffer.label") - - private val logic = Isabelle_Logic.logic_selector(true) - - private val controls = - new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic) - add(controls.peer, BorderLayout.NORTH) - - - /* component state -- owned by Swing thread */ - - private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty - - private object Node_Renderer_Component extends Label - { - opaque = false - xAlignment = Alignment.Leading - border = BorderFactory.createEmptyBorder(2, 2, 2, 2) - - var node_name = Document.Node.Name.empty - override def paintComponent(gfx: Graphics2D) - { - nodes_status.get(node_name) match { - case Some(st) if st.total > 0 => - val size = peer.getSize() - val insets = border.getBorderInsets(this.peer) - val w = size.width - insets.left - insets.right - val h = size.height - insets.top - insets.bottom - var end = size.width - insets.right - for { - (n, color) <- List( - (st.unprocessed, PIDE.options.color_value("unprocessed1_color")), - (st.running, PIDE.options.color_value("running_color")), - (st.warned, PIDE.options.color_value("warning_color")), - (st.failed, PIDE.options.color_value("error_color"))) } - { - gfx.setColor(color) - val v = (n * w / st.total) max (if (n > 0) 2 else 0) - gfx.fillRect(end - v, insets.top, v, h) - end -= v - } - case _ => - } - super.paintComponent(gfx) - } - } - - private class Node_Renderer extends ListView.Renderer[Document.Node.Name] - { - def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean, - name: Document.Node.Name, index: Int): Component = - { - val component = Node_Renderer_Component - component.node_name = name - component.text = name.theory - component - } - } - status.renderer = new Node_Renderer - - private def handle_update(restriction: Option[Set[Document.Node.Name]] = None) - { - Swing_Thread.now { - val snapshot = PIDE.session.snapshot() - - val iterator = - restriction match { - case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name))) - case None => snapshot.version.nodes.entries - } - val nodes_status1 = - (nodes_status /: iterator)({ case (status, (name, node)) => - if (PIDE.thy_load.loaded_theories(name.theory)) status - else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) }) - - if (nodes_status != nodes_status1) { - nodes_status = nodes_status1 - status.listData = - snapshot.version.nodes.topological_order.filter( - (name: Document.Node.Name) => nodes_status.isDefinedAt(name)) - } - } - } - - - /* main actor */ - - private val main_actor = actor { - loop { - react { - case phase: Session.Phase => handle_phase(phase) - - case _: Session.Global_Options => Swing_Thread.later { logic.load () } - - case changed: Session.Commands_Changed => handle_update(Some(changed.nodes)) - - case bad => System.err.println("Session_Dockable: ignoring bad message " + bad) - } - } - } - - override def init() - { - PIDE.session.phase_changed += main_actor; handle_phase(PIDE.session.phase) - PIDE.session.global_options += main_actor - PIDE.session.commands_changed += main_actor; handle_update() - } - - override def exit() - { - PIDE.session.phase_changed -= main_actor - PIDE.session.global_options -= main_actor - PIDE.session.commands_changed -= main_actor - } -} diff -r 1426d478ccda -r f70b3712040f src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Fri Nov 30 21:28:35 2012 +0100 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Fri Nov 30 21:30:24 2012 +0100 @@ -10,16 +10,18 @@ import isabelle._ import java.awt.Font -import org.gjt.sp.jedit.View import scala.swing.event.ValueChanged import scala.swing.{Action, Button, FlowPanel, TabbedPane, TextField, BorderPanel, Label} +import org.gjt.sp.jedit.View + + class Symbols_Dockable(view: View, position: String) extends Dockable(view, position) { val searchspace = for ((group, symbols) <- Symbol.groups; sym <- symbols) - yield (sym, sym.toLowerCase) + yield (sym, Library.lowercase(sym)) private class Symbol_Component(val symbol: String) extends Button { @@ -75,7 +77,8 @@ val max_results = PIDE.options.int("jedit_symbols_search_limit") max 0 results_panel.contents.clear val results = - (searchspace filter (search.text.toLowerCase.split("\\s+") forall _._2.contains) + (searchspace filter + (Library.lowercase(search.text).split("\\s+") forall _._2.contains) take (max_results + 1)).toList for ((sym, _) <- results) results_panel.contents += new Symbol_Component(sym) diff -r 1426d478ccda -r f70b3712040f src/Tools/jEdit/src/theories_dockable.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/theories_dockable.scala Fri Nov 30 21:30:24 2012 +0100 @@ -0,0 +1,179 @@ +/* Title: Tools/jEdit/src/theories_dockable.scala + Author: Makarius + +Dockable window for theories managed by prover. +*/ + +package isabelle.jedit + + +import isabelle._ + +import scala.actors.Actor._ +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component} +import scala.swing.event.{ButtonClicked, MouseClicked} + +import java.lang.System +import java.awt.{BorderLayout, Graphics2D, Insets} +import javax.swing.{JList, BorderFactory} +import javax.swing.border.{BevelBorder, SoftBevelBorder} + +import org.gjt.sp.jedit.{View, jEdit} + + +class Theories_Dockable(view: View, position: String) extends Dockable(view, position) +{ + /* status */ + + private val status = new ListView(Nil: List[Document.Node.Name]) { + listenTo(mouse.clicks) + reactions += { + case MouseClicked(_, point, _, clicks, _) if clicks == 2 => + val index = peer.locationToIndex(point) + if (index >= 0) jEdit.openFile(view, listData(index).node) + } + } + status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP) + status.peer.setVisibleRowCount(0) + status.selection.intervalMode = ListView.IntervalMode.Single + + set_content(new ScrollPane(status)) + + + /* controls */ + + def phase_text(phase: Session.Phase): String = + "Prover: " + Library.lowercase(phase.toString) + + private val session_phase = new Label(phase_text(PIDE.session.phase)) + session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED) + session_phase.tooltip = "Status of prover session" + + private def handle_phase(phase: Session.Phase) + { + Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " } + } + + private val cancel = new Button("Cancel") { + reactions += { case ButtonClicked(_) => PIDE.cancel_execution() } + } + cancel.tooltip = jEdit.getProperty("isabelle.cancel-execution.label") + + private val check = new Button("Check") { + reactions += { case ButtonClicked(_) => PIDE.check_buffer(view.getBuffer) } + } + check.tooltip = jEdit.getProperty("isabelle.check-buffer.label") + + private val logic = Isabelle_Logic.logic_selector(true) + + private val controls = + new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic) + add(controls.peer, BorderLayout.NORTH) + + + /* component state -- owned by Swing thread */ + + private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty + + private object Node_Renderer_Component extends Label + { + opaque = false + xAlignment = Alignment.Leading + border = BorderFactory.createEmptyBorder(2, 2, 2, 2) + + var node_name = Document.Node.Name.empty + override def paintComponent(gfx: Graphics2D) + { + nodes_status.get(node_name) match { + case Some(st) if st.total > 0 => + val size = peer.getSize() + val insets = border.getBorderInsets(this.peer) + val w = size.width - insets.left - insets.right + val h = size.height - insets.top - insets.bottom + var end = size.width - insets.right + for { + (n, color) <- List( + (st.unprocessed, PIDE.options.color_value("unprocessed1_color")), + (st.running, PIDE.options.color_value("running_color")), + (st.warned, PIDE.options.color_value("warning_color")), + (st.failed, PIDE.options.color_value("error_color"))) } + { + gfx.setColor(color) + val v = (n * w / st.total) max (if (n > 0) 2 else 0) + gfx.fillRect(end - v, insets.top, v, h) + end -= v + } + case _ => + } + super.paintComponent(gfx) + } + } + + private class Node_Renderer extends ListView.Renderer[Document.Node.Name] + { + def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean, + name: Document.Node.Name, index: Int): Component = + { + val component = Node_Renderer_Component + component.node_name = name + component.text = name.theory + component + } + } + status.renderer = new Node_Renderer + + private def handle_update(restriction: Option[Set[Document.Node.Name]] = None) + { + Swing_Thread.now { + val snapshot = PIDE.session.snapshot() + + val iterator = + restriction match { + case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name))) + case None => snapshot.version.nodes.entries + } + val nodes_status1 = + (nodes_status /: iterator)({ case (status, (name, node)) => + if (PIDE.thy_load.loaded_theories(name.theory)) status + else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) }) + + if (nodes_status != nodes_status1) { + nodes_status = nodes_status1 + status.listData = + snapshot.version.nodes.topological_order.filter( + (name: Document.Node.Name) => nodes_status.isDefinedAt(name)) + } + } + } + + + /* main actor */ + + private val main_actor = actor { + loop { + react { + case phase: Session.Phase => handle_phase(phase) + + case _: Session.Global_Options => Swing_Thread.later { logic.load () } + + case changed: Session.Commands_Changed => handle_update(Some(changed.nodes)) + + case bad => System.err.println("Theories_Dockable: ignoring bad message " + bad) + } + } + } + + override def init() + { + PIDE.session.phase_changed += main_actor; handle_phase(PIDE.session.phase) + PIDE.session.global_options += main_actor + PIDE.session.commands_changed += main_actor; handle_update() + } + + override def exit() + { + PIDE.session.phase_changed -= main_actor + PIDE.session.global_options -= main_actor + PIDE.session.commands_changed -= main_actor + } +}