diff --git a/src/Tools/jEdit/src/isabelle_options.scala b/src/Tools/jEdit/src/isabelle_options.scala --- a/src/Tools/jEdit/src/isabelle_options.scala +++ b/src/Tools/jEdit/src/isabelle_options.scala @@ -1,61 +1,61 @@ /* Title: Tools/jEdit/src/isabelle_options.scala Author: Makarius Editor pane for plugin options. */ package isabelle.jedit import isabelle._ import org.gjt.sp.jedit.{jEdit, AbstractOptionPane} abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name) { protected val components: List[(String, List[Option_Component])] override def _init(): Unit = { val dummy_property = "options.isabelle.dummy" for ((s, cs) <- components) { if (s != "") { jEdit.setProperty(dummy_property, s) addSeparator(dummy_property) jEdit.setProperty(dummy_property, null) } cs.foreach(c => addComponent(c.title, c.peer)) } } override def _save(): Unit = { for ((_, cs) <- components) cs.foreach(_.save()) } } class Isabelle_Options1 extends Isabelle_Options("isabelle-general") { val options: JEdit_Options = PIDE.options private val predefined = - List(JEdit_Sessions.logic_selector(options, false), + List(JEdit_Sessions.logic_selector(options), JEdit_Spell_Checker.dictionaries_selector()) protected val components = options.make_components(predefined, (for ((name, opt) <- options.value.options.iterator if opt.public) yield name).toSet) } class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering") { private val predefined = (for { (name, opt) <- PIDE.options.value.options.toList if (name.endsWith("_color") && opt.section == JEdit_Options.RENDERING_SECTION) } yield PIDE.options.make_color_component(opt)) assert(predefined.nonEmpty) protected val components = PIDE.options.make_components(predefined, _ => false) } diff --git a/src/Tools/jEdit/src/jedit_sessions.scala b/src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala +++ b/src/Tools/jEdit/src/jedit_sessions.scala @@ -1,150 +1,150 @@ /* Title: Tools/jEdit/src/jedit_sessions.scala Author: Makarius Isabelle/jEdit session information, based on implicit process environment and explicit options. */ package isabelle.jedit import isabelle._ import scala.swing.ComboBox import scala.swing.event.SelectionChanged object JEdit_Sessions { /* session options */ def session_dirs: List[Path] = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).filterNot(p => p.implode == "-") def session_no_build: Boolean = Isabelle_System.getenv("JEDIT_NO_BUILD") == "true" def session_options(options: Options): Options = { val options1 = Isabelle_System.getenv("JEDIT_BUILD_MODE") match { case "default" => options case mode => options.bool.update("system_heaps", mode == "system") } val options2 = Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match { case "" => options1 case s => options1.string.update("ML_process_policy", s) } options2 } def sessions_structure( options: Options = PIDE.options.value, dirs: List[Path] = session_dirs ): Sessions.Structure = { Sessions.load_structure(session_options(options), dirs = dirs) } /* raw logic info */ private val jedit_logic_option = "jedit_logic" def logic_name(options: Options): String = Isabelle_System.default_logic( Isabelle_System.getenv("JEDIT_LOGIC"), options.string(jedit_logic_option)) def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR")) def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true" def logic_include_sessions: List[String] = space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS")) def logic_info(options: Options): Option[Sessions.Info] = try { sessions_structure(options = options).get(logic_name(options)) } catch { case ERROR(_) => None } def logic_root(options: Options): Position.T = if (logic_requirements) logic_info(options).map(_.pos) getOrElse Position.none else Position.none /* logic selector */ - private class Logic_Entry(val name: String, val description: String) { - override def toString: String = description + private sealed case class Logic_Entry(name: String = "", description: String = "") { + override def toString: String = proper_string(description) getOrElse name } - def logic_selector(options: Options_Variable, autosave: Boolean): Option_Component = { + def logic_selector(options: Options_Variable, autosave: Boolean = false): Option_Component = { GUI_Thread.require {} - val session_list = { + val default_entry = Logic_Entry(description = "default (" + logic_name(options.value) + ")") + + val session_entries = { val sessions = sessions_structure(options = options.value) val (main_sessions, other_sessions) = sessions.imports_topological_order.partition(name => sessions(name).groups.contains("main")) - main_sessions.sorted ::: other_sessions.sorted + (main_sessions.sorted ::: other_sessions.sorted).map(name => Logic_Entry(name = name)) } - val entries = - new Logic_Entry("", "default (" + logic_name(options.value) + ")") :: - session_list.map(name => new Logic_Entry(name, name)) + val entries = default_entry :: session_entries new ComboBox(entries) with Option_Component { name = jedit_logic_option tooltip = "Logic session name (change requires restart)" val title = "Logic" def load(): Unit = { val logic = options.string(jedit_logic_option) entries.find(_.name == logic) match { case Some(entry) => selection.item = entry case None => } } def save(): Unit = options.string(jedit_logic_option) = selection.item.name load() if (autosave) { listenTo(selection) reactions += { case SelectionChanged(_) => save() } } } } /* session build process */ def session_base_info(options: Options): Sessions.Base_Info = Sessions.base_info(options, dirs = JEdit_Sessions.session_dirs, include_sessions = logic_include_sessions, session = logic_name(options), session_ancestor = logic_ancestor, session_requirements = logic_requirements) def session_build( options: Options, progress: Progress = new Progress, no_build: Boolean = false ): Int = { Build.build(session_options(options), selection = Sessions.Selection.session(PIDE.resources.session_base.session_name), progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs, infos = PIDE.resources.session_base_info.infos).rc } def session_start(options0: Options): Unit = { val session = PIDE.session val options = session_options(options0) val sessions_structure = PIDE.resources.session_base_info.sessions_structure val store = Sessions.store(options) session.phase_changed += PIDE.plugin.session_phase_changed Isabelle_Process.start(session, options, sessions_structure, store, logic = PIDE.resources.session_base.session_name, modes = (space_explode(',', options.string("jedit_print_mode")) ::: space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse) } } diff --git a/src/Tools/jEdit/src/theories_dockable.scala b/src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala +++ b/src/Tools/jEdit/src/theories_dockable.scala @@ -1,268 +1,268 @@ /* Title: Tools/jEdit/src/theories_dockable.scala Author: Makarius Dockable window for theories managed by prover. */ package isabelle.jedit import isabelle._ import scala.swing.{Button, TextArea, Label, ListView, Alignment, ScrollPane, Component, CheckBox, BorderPanel} import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved} import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension} import javax.swing.{JList, BorderFactory, UIManager} 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(List.empty[Document.Node.Name]) { background = { // enforce default value val c = UIManager.getDefaults.getColor("Panel.background") new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha) } listenTo(mouse.clicks) listenTo(mouse.moves) reactions += { case MouseClicked(_, point, _, clicks, _) => val index = peer.locationToIndex(point) if (index >= 0) { if (in_checkbox(peer.indexToLocation(index), point)) { if (clicks == 1) Document_Model.node_required(listData(index), toggle = true) } else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node) } case MouseMoved(_, point, _) => val index = peer.locationToIndex(point) val index_location = peer.indexToLocation(index) if (index >= 0 && in_checkbox(index_location, point)) tooltip = "Mark as required for continuous checking" else if (index >= 0 && in_label(index_location, point)) { val name = listData(index) val st = nodes_status.overall_node_status(name) tooltip = "theory " + quote(name.theory) + (if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")") } else tooltip = null } } 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: " + phase.print 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): Unit = { GUI_Thread.require {} session_phase.text = " " + phase_text(phase) + " " } private val purge = new Button("Purge") { tooltip = "Restrict document model to theories required for open editor buffers" reactions += { case ButtonClicked(_) => PIDE.editor.purge() } } private val continuous_checking = new Isabelle.Continuous_Checking continuous_checking.focusable = false - private val logic = JEdit_Sessions.logic_selector(PIDE.options, true) + private val logic = JEdit_Sessions.logic_selector(PIDE.options, autosave = true) private val controls = Wrap_Panel(List(purge, continuous_checking, session_phase, logic)) add(controls.peer, BorderLayout.NORTH) /* component state -- owned by GUI thread */ private var nodes_status = Document_Status.Nodes_Status.empty private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes() private def in(geometry: Option[(Point, Dimension)], loc0: Point, p: Point): Boolean = geometry match { case Some((loc, size)) => loc0.x + loc.x <= p.x && p.x < loc0.x + size.width && loc0.y + loc.y <= p.y && p.y < loc0.y + size.height case None => false } private def in_checkbox(loc0: Point, p: Point): Boolean = Node_Renderer_Component != null && in(Node_Renderer_Component.checkbox_geometry, loc0, p) private def in_label(loc0: Point, p: Point): Boolean = Node_Renderer_Component != null && in(Node_Renderer_Component.label_geometry, loc0, p) private object Node_Renderer_Component extends BorderPanel { opaque = true border = BorderFactory.createEmptyBorder(2, 2, 2, 2) var node_name = Document.Node.Name.empty var checkbox_geometry: Option[(Point, Dimension)] = None val checkbox = new CheckBox { opaque = false override def paintComponent(gfx: Graphics2D): Unit = { super.paintComponent(gfx) if (location != null && size != null) checkbox_geometry = Some((location, size)) } } var label_geometry: Option[(Point, Dimension)] = None val label = new Label { background = view.getTextArea.getPainter.getBackground foreground = view.getTextArea.getPainter.getForeground opaque = false xAlignment = Alignment.Leading override def paintComponent(gfx: Graphics2D): Unit = { def paint_segment(x: Int, w: Int, color: Color): Unit = { gfx.setColor(color) gfx.fillRect(x, 0, w, size.height) } paint_segment(0, size.width, background) nodes_status.get(node_name) match { case Some(node_status) => val segments = List( (node_status.unprocessed, PIDE.options.color_value("unprocessed1_color")), (node_status.running, PIDE.options.color_value("running_color")), (node_status.warned, PIDE.options.color_value("warning_color")), (node_status.failed, PIDE.options.color_value("error_color")) ).filter(_._1 > 0) segments.foldLeft(size.width - 2) { case (last, (n, color)) => val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4 paint_segment(last - w, w, color) last - w - 1 } case None => paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color")) } super.paintComponent(gfx) if (location != null && size != null) label_geometry = Some((location, size)) } } def label_border(name: Document.Node.Name): Unit = { val st = nodes_status.overall_node_status(name) val color = st match { case Document_Status.Overall_Node_Status.ok => PIDE.options.color_value("ok_color") case Document_Status.Overall_Node_Status.failed => PIDE.options.color_value("failed_color") case _ => label.foreground } val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 3 val thickness2 = 4 - thickness1 label.border = BorderFactory.createCompoundBorder( BorderFactory.createLineBorder(color, thickness1), BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2)) } layout(checkbox) = BorderPanel.Position.West layout(label) = BorderPanel.Position.Center } private class Node_Renderer extends ListView.Renderer[Document.Node.Name] { def componentFor( list: ListView[_ <: isabelle.Document.Node.Name], isSelected: Boolean, focused: Boolean, name: Document.Node.Name, index: Int ): Component = { val component = Node_Renderer_Component component.node_name = name component.checkbox.selected = nodes_required.contains(name) component.label_border(name) component.label.text = name.theory_base_name component } } status.renderer = new Node_Renderer private def handle_update( domain: Option[Set[Document.Node.Name]] = None, trim: Boolean = false ): Unit = { GUI_Thread.require {} val snapshot = PIDE.session.snapshot() val (nodes_status_changed, nodes_status1) = nodes_status.update( PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim) nodes_status = nodes_status1 if (nodes_status_changed) { status.listData = (for { (name, node_status) <- nodes_status1.present.iterator if !node_status.is_suppressed && node_status.total > 0 } yield name).toList } } /* main */ private val main = Session.Consumer[Any](getClass.getName) { case phase: Session.Phase => GUI_Thread.later { handle_phase(phase) } case _: Session.Global_Options => GUI_Thread.later { continuous_checking.load() logic.load () nodes_required = Document_Model.required_nodes() status.repaint() } case changed: Session.Commands_Changed => GUI_Thread.later { handle_update(domain = Some(changed.nodes), trim = changed.assignment) } } override def init(): Unit = { PIDE.session.phase_changed += main PIDE.session.global_options += main PIDE.session.commands_changed += main handle_phase(PIDE.session.phase) handle_update() } override def exit(): Unit = { PIDE.session.phase_changed -= main PIDE.session.global_options -= main PIDE.session.commands_changed -= main } }