--- a/etc/build.props Fri Aug 12 15:35:07 2022 +0200
+++ b/etc/build.props Fri Aug 12 20:21:09 2022 +0200
@@ -236,6 +236,7 @@
src/Tools/jEdit/src/context_menu.scala \
src/Tools/jEdit/src/debugger_dockable.scala \
src/Tools/jEdit/src/dockable.scala \
+ src/Tools/jEdit/src/document_dockable.scala \
src/Tools/jEdit/src/document_model.scala \
src/Tools/jEdit/src/document_view.scala \
src/Tools/jEdit/src/documentation_dockable.scala \
--- a/src/Pure/GUI/gui.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Pure/GUI/gui.scala Fri Aug 12 20:21:09 2022 +0200
@@ -118,7 +118,7 @@
abstract class Zoom_Box extends ComboBox[String](
List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")
) {
- def changed: Unit
+ def changed(): Unit
def factor: Int = parse(selection.item)
private def parse(text: String): Int =
@@ -147,7 +147,7 @@
selection.index = 3
listenTo(selection)
- reactions += { case SelectionChanged(_) => changed }
+ reactions += { case SelectionChanged(_) => changed() }
}
--- a/src/Pure/General/file.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Pure/General/file.scala Fri Aug 12 20:21:09 2022 +0200
@@ -301,19 +301,13 @@
/* content */
- object Content {
- def apply(path: Path, content: Bytes): Content_Bytes = new Content_Bytes(path, content)
- def apply(path: Path, content: String): Content_String = new Content_String(path, content)
- def apply(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content)
- }
+ def content(path: Path, content: Bytes): Content = new Content(path, content)
+ def content(path: Path, content: String): Content = new Content(path, Bytes(content))
+ def content(path: Path, content: XML.Body): Content_XML = new Content_XML(path, content)
- trait Content {
- def path: Path
- def write(dir: Path): Unit
+ final class Content private[File](val path: Path, val content: Bytes) {
override def toString: String = path.toString
- }
- final class Content_Bytes private[File](val path: Path, val content: Bytes) extends Content {
def write(dir: Path): Unit = {
val full_path = dir + path
Isabelle_System.make_directory(full_path.expand.dir)
@@ -321,16 +315,9 @@
}
}
- final class Content_String private[File](val path: Path, val content: String) extends Content {
- def write(dir: Path): Unit = {
- val full_path = dir + path
- Isabelle_System.make_directory(full_path.expand.dir)
- File.write(full_path, content)
- }
- }
+ final class Content_XML private[File](val path: Path, val content: XML.Body) {
+ override def toString: String = path.toString
- final class Content_XML private[File](val path: Path, val content: XML.Body) {
- def output(out: XML.Body => String): Content_String =
- new Content_String(path, out(content))
+ def output(out: XML.Body => String): Content = new Content(path, Bytes(out(content)))
}
}
--- a/src/Pure/General/mercurial.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Pure/General/mercurial.scala Fri Aug 12 20:21:09 2022 +0200
@@ -323,10 +323,10 @@
Rsync.init(context0, target,
contents =
- File.Content(Hg_Sync.PATH_ID, id_content) ::
- File.Content(Hg_Sync.PATH_LOG, log_content) ::
- File.Content(Hg_Sync.PATH_DIFF, diff_content) ::
- File.Content(Hg_Sync.PATH_STAT, stat_content) :: contents)
+ File.content(Hg_Sync.PATH_ID, id_content) ::
+ File.content(Hg_Sync.PATH_LOG, log_content) ::
+ File.content(Hg_Sync.PATH_DIFF, diff_content) ::
+ File.content(Hg_Sync.PATH_STAT, stat_content) :: contents)
val (exclude, source) =
if (rev.isEmpty) {
--- a/src/Pure/PIDE/document.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Pure/PIDE/document.scala Fri Aug 12 20:21:09 2022 +0200
@@ -78,9 +78,6 @@
abbrevs: Thy_Header.Abbrevs = Nil,
errors: List[String] = Nil
) {
- def imports_offset: Map[Int, Name] =
- (for { (name, Position.Offset(i)) <- imports_pos } yield i -> name).toMap
-
def imports: List[Name] = imports_pos.map(_._1)
def append_errors(msgs: List[String]): Header =
@@ -341,7 +338,7 @@
def source: String =
get_blob match {
case Some(blob) => blob.source
- case None => command_iterator(0).map({ case (cmd, _) => cmd.source }).mkString
+ case None => command_iterator().map({ case (cmd, _) => cmd.source }).mkString
}
}
@@ -689,12 +686,6 @@
state.command_results(version, command)
- /* command ids: static and dynamic */
-
- def command_id_map: Map[Document_ID.Generic, Command] =
- state.command_id_map(version, get_node(node_name).commands)
-
-
/* cumulate markup */
def cumulate[A](
@@ -1093,18 +1084,6 @@
removing_versions = false)
}
- def command_id_map(
- version: Version,
- commands: Iterable[Command]
- ) : Map[Document_ID.Generic, Command] = {
- require(is_assigned(version), "version not assigned (command_id_map)")
- val assignment = the_assignment(version).check_finished
- (for {
- command <- commands.iterator
- id <- (command.id :: assignment.command_execs.getOrElse(command.id, Nil)).iterator
- } yield (id -> command)).toMap
- }
-
def command_maybe_consolidated(version: Version, command: Command): Boolean = {
require(is_assigned(version), "version not assigned (command_maybe_consolidated)")
try {
--- a/src/Pure/System/classpath.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Pure/System/classpath.scala Fri Aug 12 20:21:09 2022 +0200
@@ -20,7 +20,7 @@
def apply(
jar_files: List[JFile] = Nil,
- jar_contents: List[File.Content_Bytes] = Nil): Classpath =
+ jar_contents: List[File.Content] = Nil): Classpath =
{
val jar_files0 =
for {
--- a/src/Pure/Thy/document_build.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Pure/Thy/document_build.scala Fri Aug 12 20:21:09 2022 +0200
@@ -31,10 +31,12 @@
}
sealed case class Document_Input(name: String, sources: SHA1.Digest)
- extends Document_Name
+ extends Document_Name { override def toString: String = name }
sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes)
extends Document_Name {
+ override def toString: String = name
+
def log: String = log_xz.uncompress().text
def log_lines: List[String] = split_lines(log)
@@ -117,23 +119,29 @@
def context(
session_context: Export.Session_Context,
+ document_session: Option[Sessions.Base] = None,
progress: Progress = new Progress
- ): Context = new Context(session_context, progress)
+ ): Context = new Context(session_context, document_session, progress)
final class Context private[Document_Build](
- val session_context: Export.Session_Context,
+ session_context: Export.Session_Context,
+ document_session: Option[Sessions.Base],
val progress: Progress = new Progress
) {
+ context =>
+
+
/* session info */
- def session: String = session_context.session_name
+ private val base = document_session getOrElse session_context.session_base
+ private val info = session_context.sessions_structure(base.session_name)
- private val info = session_context.sessions_structure(session)
- private val base = session_context.session_base
+ def session: String = info.name
+ def options: Options = info.options
- val classpath: List[File.Content_Bytes] = session_context.classpath()
+ override def toString: String = session
- def options: Options = info.options
+ val classpath: List[File.Content] = session_context.classpath()
def document_bibliography: Boolean = options.bool("document_bibliography")
@@ -168,13 +176,13 @@
val path = Path.basic(tex_name(name))
val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
val content = YXML.parse_body(entry.text)
- File.Content(path, content)
+ File.content(path, content)
}
lazy val session_graph: File.Content = {
val path = Presentation.session_graph_path
val content = graphview.Graph_File.make_pdf(options, base.session_graph_display)
- File.Content(path, content)
+ File.content(path, content)
}
lazy val session_tex: File.Content = {
@@ -182,7 +190,7 @@
val content =
Library.terminate_lines(
base.proper_session_theories.map(name => "\\input{" + tex_name(name) + "}"))
- File.Content(path, content)
+ File.content(path, content)
}
lazy val isabelle_logo: Option[File.Content] = {
@@ -191,11 +199,22 @@
Logo.create_logo(logo_name, output_file = tmp_path, quiet = true)
val path = Path.basic("isabelle_logo.pdf")
val content = Bytes.read(tmp_path)
- File.Content(path, content)
+ File.content(path, content)
})
}
+ /* build document */
+
+ def build_document(doc: Document_Variant, verbose: Boolean = false): Document_Output = {
+ Isabelle_System.with_tmp_dir("document") { tmp_dir =>
+ val engine = get_engine()
+ val directory = engine.prepare_directory(context, tmp_dir, doc)
+ engine.build_document(context, directory, verbose)
+ }
+ }
+
+
/* document directory */
def prepare_directory(
--- a/src/Pure/Thy/export.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Pure/Thy/export.scala Fri Aug 12 20:21:09 2022 +0200
@@ -411,7 +411,7 @@
def theory(theory: String, other_cache: Option[Term.Cache] = None): Theory_Context =
new Theory_Context(session_context, theory, other_cache)
- def classpath(): List[File.Content_Bytes] = {
+ def classpath(): List[File.Content] = {
(for {
session <- session_stack.iterator
info <- sessions_structure.get(session).iterator
@@ -420,7 +420,7 @@
entry_name <- entry_names(session = session).iterator
if matcher(entry_name)
entry <- get(entry_name.theory, entry_name.name).iterator
- } yield File.Content(entry.entry_name.make_path(), entry.uncompressed)).toList
+ } yield File.content(entry.entry_name.make_path(), entry.uncompressed)).toList
}
override def toString: String =
--- a/src/Pure/Thy/latex.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Pure/Thy/latex.scala Fri Aug 12 20:21:09 2022 +0200
@@ -133,7 +133,7 @@
val tags =
(for ((name, op) <- map.iterator)
yield "\\isa" + op + "tag{" + name + "}").toList
- File.Content(path, comment + """
+ File.content(path, comment + """
\newcommand{\isakeeptag}[1]%
{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
--- a/src/Pure/Tools/sync.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Pure/Tools/sync.scala Fri Aug 12 20:21:09 2022 +0200
@@ -59,7 +59,7 @@
context.progress.echo_if(verbose, "\n* Isabelle repository:")
val filter_heaps = if (purge_heaps) Nil else List("protect /heaps", "protect /heaps/**")
sync(hg, target, rev,
- contents = List(File.Content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))),
+ contents = List(File.content(Path.explode("etc/ISABELLE_ID"), hg.id(rev = rev))),
filter = filter_heaps ::: List("protect /AFP"))
for (hg <- afp_hg) {
--- a/src/Tools/Graphview/graph_panel.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/Graphview/graph_panel.scala Fri Aug 12 20:21:09 2022 +0200
@@ -298,7 +298,7 @@
tooltip = "Save current graph layout as PNG or PDF"
}
- private val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) }
+ private val zoom = new GUI.Zoom_Box { def changed(): Unit = rescale(0.01 * factor) }
private val fit_window = new Button {
action = Action("Fit to window") { fit_to_window() }
--- a/src/Tools/Graphview/tree_panel.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/Graphview/tree_panel.scala Fri Aug 12 20:21:09 2022 +0200
@@ -73,7 +73,7 @@
tree.addKeyListener(new KeyAdapter {
override def keyPressed(e: KeyEvent): Unit =
if (e.getKeyCode == KeyEvent.VK_ENTER) {
- e.consume
+ e.consume()
selection_action()
}
})
--- a/src/Tools/VSCode/src/build_vscodium.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/VSCode/src/build_vscodium.scala Fri Aug 12 20:21:09 2022 +0200
@@ -37,7 +37,7 @@
"abbrevs" -> entry.abbrevs) ++
JSON.optional("code", entry.code))
- File.Content(Path.explode("symbols.json"), symbols_js)
+ File.content(Path.explode("symbols.json"), symbols_js)
}
def make_isabelle_encoding(header: String): File.Content = {
@@ -51,7 +51,7 @@
val body =
File.read(Path.explode("$ISABELLE_VSCODE_HOME/patches") + path)
.replace("[/*symbols*/]", symbols_js)
- File.Content(path, header + "\n" + body)
+ File.content(path, header + "\n" + body)
}
--- a/src/Tools/jEdit/jedit_main/dockables.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/dockables.scala Fri Aug 12 20:21:09 2022 +0200
@@ -13,6 +13,9 @@
class Debugger_Dockable(view: View, position: String)
extends isabelle.jedit.Debugger_Dockable(view, position)
+class Document_Dockable(view: View, position: String)
+ extends isabelle.jedit.Document_Dockable(view, position)
+
class Documentation_Dockable(view: View, position: String)
extends isabelle.jedit.Documentation_Dockable(view, position)
--- a/src/Tools/jEdit/jedit_main/dockables.xml Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/dockables.xml Fri Aug 12 20:21:09 2022 +0200
@@ -5,6 +5,9 @@
<DOCKABLE NAME="isabelle-debugger" MOVABLE="TRUE">
new isabelle.jedit_main.Debugger_Dockable(view, position);
</DOCKABLE>
+ <DOCKABLE NAME="isabelle-document" MOVABLE="TRUE">
+ new isabelle.jedit_main.Document_Dockable(view, position);
+ </DOCKABLE>
<DOCKABLE NAME="isabelle-documentation" MOVABLE="TRUE">
new isabelle.jedit_main.Documentation_Dockable(view, position);
</DOCKABLE>
--- a/src/Tools/jEdit/jedit_main/plugin.props Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/plugin.props Fri Aug 12 20:21:09 2022 +0200
@@ -37,6 +37,7 @@
isabelle.java-monitor \
- \
isabelle-debugger \
+ isabelle-document \
isabelle-documentation \
isabelle-monitor \
isabelle-output \
@@ -52,6 +53,8 @@
isabelle-timing
isabelle-debugger.label=Debugger panel
isabelle-debugger.title=Debugger
+isabelle-document.label=Document panel
+isabelle-document.title=Document
isabelle-documentation.label=Documentation panel
isabelle-documentation.title=Documentation
isabelle-graphview.label=Graphview panel
--- a/src/Tools/jEdit/src/completion_popup.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Fri Aug 12 20:21:09 2022 +0200
@@ -517,12 +517,12 @@
case KeyEvent.KEY_PRESSED =>
val key_code = evt.getKeyCode
if (key_code == KeyEvent.VK_ESCAPE) {
- if (dismissed()) evt.consume
+ if (dismissed()) evt.consume()
}
case KeyEvent.KEY_TYPED =>
super.processKeyEvent(evt)
process(evt)
- evt.consume
+ evt.consume()
case _ =>
}
if (!evt.isConsumed) super.processKeyEvent(evt)
@@ -598,26 +598,26 @@
if (!e.isConsumed) {
e.getKeyCode match {
case KeyEvent.VK_ENTER if PIDE.options.bool("jedit_completion_select_enter") =>
- if (complete_selected()) e.consume
+ if (complete_selected()) e.consume()
hide_popup()
case KeyEvent.VK_TAB if PIDE.options.bool("jedit_completion_select_tab") =>
- if (complete_selected()) e.consume
+ if (complete_selected()) e.consume()
hide_popup()
case KeyEvent.VK_ESCAPE =>
hide_popup()
- e.consume
+ e.consume()
case KeyEvent.VK_UP | KeyEvent.VK_KP_UP if multi =>
move_items(-1)
- e.consume
+ e.consume()
case KeyEvent.VK_DOWN | KeyEvent.VK_KP_DOWN if multi =>
move_items(1)
- e.consume
+ e.consume()
case KeyEvent.VK_PAGE_UP if multi =>
move_pages(-1)
- e.consume
+ e.consume()
case KeyEvent.VK_PAGE_DOWN if multi =>
move_pages(1)
- e.consume
+ e.consume()
case _ =>
if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown)
hide_popup()
@@ -632,7 +632,7 @@
list_view.peer.addMouseListener(new MouseAdapter {
override def mouseClicked(e: MouseEvent): Unit = {
- if (complete_selected()) e.consume
+ if (complete_selected()) e.consume()
hide_popup()
}
})
--- a/src/Tools/jEdit/src/debugger_dockable.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Fri Aug 12 20:21:09 2022 +0200
@@ -72,12 +72,8 @@
override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
- private def handle_resize(): Unit = {
- GUI_Thread.require {}
-
- pretty_text_area.resize(
- Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
- }
+ private def handle_resize(): Unit =
+ GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
private def handle_update(): Unit = {
GUI_Thread.require {}
@@ -85,11 +81,11 @@
val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
val (new_threads, new_output) = debugger.status(tree_selection())
- if (new_threads != current_threads)
- update_tree(new_threads)
+ if (new_threads != current_threads) update_tree(new_threads)
- if (new_output != current_output)
+ if (new_output != current_output) {
pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output))
+ }
current_snapshot = new_snapshot
current_threads = new_threads
@@ -130,12 +126,12 @@
case _ => thread_contexts.headOption
}
- tree.clearSelection
- root.removeAllChildren
+ tree.clearSelection()
+ root.removeAllChildren()
for (thread <- thread_contexts) {
val thread_node = new DefaultMutableTreeNode(thread)
- for ((debug_state, i) <- thread.debug_states.zipWithIndex)
+ for ((_, i) <- thread.debug_states.zipWithIndex)
thread_node.add(new DefaultMutableTreeNode(thread.select(i)))
root.add(thread_node)
}
@@ -167,19 +163,15 @@
}
}
- tree.addTreeSelectionListener(
- new TreeSelectionListener {
- override def valueChanged(e: TreeSelectionEvent): Unit = {
- update_focus()
- update_vals()
- }
- })
+ tree.addTreeSelectionListener({ (_: TreeSelectionEvent) =>
+ update_focus()
+ update_vals()
+ })
tree.addMouseListener(
new MouseAdapter {
override def mouseClicked(e: MouseEvent): Unit = {
val click = tree.getPathForLocation(e.getX, e.getY)
- if (click != null && e.getClickCount == 1)
- update_focus()
+ if (click != null && e.getClickCount == 1) update_focus()
}
})
@@ -223,8 +215,9 @@
private val context_field =
new Completion_Popup.History_Text_Field("isabelle-debugger-context") {
override def processKeyEvent(evt: KeyEvent): Unit = {
- if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER)
+ if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) {
eval_expression()
+ }
super.processKeyEvent(evt)
}
setColumns(20)
@@ -238,8 +231,9 @@
private val expression_field =
new Completion_Popup.History_Text_Field("isabelle-debugger-expression") {
override def processKeyEvent(evt: KeyEvent): Unit = {
- if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER)
+ if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) {
eval_expression()
+ }
super.processKeyEvent(evt)
}
{ val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
@@ -268,7 +262,7 @@
selected = false
}
- private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
private val controls =
Wrap_Panel(
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/document_dockable.scala Fri Aug 12 20:21:09 2022 +0200
@@ -0,0 +1,100 @@
+/* Title: Tools/jEdit/src/document_dockable.scala
+ Author: Makarius
+
+Dockable window for document build support.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.BorderLayout
+import java.awt.event.{ComponentEvent, ComponentAdapter}
+
+import scala.swing.{ComboBox, Button}
+import scala.swing.event.{SelectionChanged, ButtonClicked}
+
+import org.gjt.sp.jedit.{jEdit, View}
+
+
+class Document_Dockable(view: View, position: String) extends Dockable(view, position) {
+ GUI_Thread.require {}
+
+
+ /* text area */
+
+ val pretty_text_area = new Pretty_Text_Area(view)
+ set_content(pretty_text_area)
+
+ override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
+
+
+ /* document build process */
+
+ private val process_indicator = new Process_Indicator
+
+
+ /* resize */
+
+ private val delay_resize =
+ Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
+
+ addComponentListener(new ComponentAdapter {
+ override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
+ })
+
+ private def handle_resize(): Unit =
+ GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
+
+
+ /* controls */
+
+ private val document_session: ComboBox[String] = {
+ new ComboBox(JEdit_Sessions.sessions_structure().build_topological_order.sorted) {
+ val title = "Session"
+ listenTo(selection)
+ reactions += { case SelectionChanged(_) => } // FIXME
+ }
+ }
+
+ private val build_button = new Button("<html><b>Build</b></html>") {
+ tooltip = "Build document"
+ reactions += { case ButtonClicked(_) =>
+ pretty_text_area.update(
+ Document.Snapshot.init, Command.Results.empty,
+ List(XML.Text(Date.now().toString))) // FIXME
+ }
+ }
+
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
+
+ private val controls =
+ Wrap_Panel(List(document_session, process_indicator.component, build_button,
+ pretty_text_area.search_label, pretty_text_area.search_field, zoom))
+
+ add(controls.peer, BorderLayout.NORTH)
+
+ override def focusOnDefaultComponent(): Unit = build_button.requestFocus()
+
+
+ /* main */
+
+ private val main =
+ Session.Consumer[Session.Global_Options](getClass.getName) {
+ case _: Session.Global_Options =>
+ GUI_Thread.later { handle_resize() }
+ }
+
+ override def init(): Unit = {
+ PIDE.session.global_options += main
+ handle_resize()
+ }
+
+ override def exit(): Unit = {
+ PIDE.session.global_options -= main
+ delay_resize.revoke()
+ }
+}
+
--- a/src/Tools/jEdit/src/document_view.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Fri Aug 12 20:21:09 2022 +0200
@@ -177,7 +177,7 @@
JEdit_Lib.key_listener(
key_pressed = { (evt: KeyEvent) =>
if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Isabelle.dismissed_popups(text_area.getView)) {
- evt.consume
+ evt.consume()
}
}
)
--- a/src/Tools/jEdit/src/documentation_dockable.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Fri Aug 12 20:21:09 2022 +0200
@@ -58,7 +58,7 @@
tree.addKeyListener(new KeyAdapter {
override def keyPressed(e: KeyEvent): Unit = {
if (e.getKeyCode == KeyEvent.VK_ENTER) {
- e.consume
+ e.consume()
val path = tree.getSelectionPath
if (path != null) {
path.getLastPathComponent match {
--- a/src/Tools/jEdit/src/info_dockable.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala Fri Aug 12 20:21:09 2022 +0200
@@ -72,14 +72,10 @@
pretty_text_area.update(snapshot, results, info)
- private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
- private def handle_resize(): Unit = {
- GUI_Thread.require {}
-
- pretty_text_area.resize(
- Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
- }
+ private def handle_resize(): Unit =
+ GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
/* resize */
@@ -106,13 +102,13 @@
}
override def init(): Unit = {
- GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
+ GUI.parent_window(this).foreach(_.addWindowFocusListener(window_focus_listener))
PIDE.session.global_options += main
handle_resize()
}
override def exit(): Unit = {
- GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
+ GUI.parent_window(this).foreach(_.removeWindowFocusListener(window_focus_listener))
PIDE.session.global_options -= main
delay_resize.revoke()
}
--- a/src/Tools/jEdit/src/isabelle.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Fri Aug 12 20:21:09 2022 +0200
@@ -108,6 +108,12 @@
case _ => None
}
+ def document_dockable(view: View): Option[Document_Dockable] =
+ wm(view).getDockableWindow("isabelle-document") match {
+ case dockable: Document_Dockable => Some(dockable)
+ case _ => None
+ }
+
def documentation_dockable(view: View): Option[Documentation_Dockable] =
wm(view).getDockableWindow("isabelle-documentation") match {
case dockable: Documentation_Dockable => Some(dockable)
--- a/src/Tools/jEdit/src/isabelle_options.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala Fri Aug 12 20:21:09 2022 +0200
@@ -38,7 +38,7 @@
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 =
--- a/src/Tools/jEdit/src/isabelle_session.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/isabelle_session.scala Fri Aug 12 20:21:09 2022 +0200
@@ -18,12 +18,6 @@
object Isabelle_Session {
- /* sessions structure */
-
- def sessions_structure(): Sessions.Structure =
- JEdit_Sessions.sessions_structure(PIDE.options.value)
-
-
/* virtual file-system */
val vfs_prefix = "isabelle-session:"
@@ -53,7 +47,7 @@
explode_url(url, component = component) match {
case None => null
case Some(elems) =>
- val sessions = sessions_structure()
+ val sessions = JEdit_Sessions.sessions_structure()
elems match {
case Nil =>
sessions.chapters.iterator.map(p => make_entry(p._1, is_dir = true)).toArray
@@ -90,7 +84,7 @@
PIDE.maybe_snapshot(view) match {
case None => ""
case Some(snapshot) =>
- val sessions = sessions_structure()
+ val sessions = JEdit_Sessions.sessions_structure()
val session = PIDE.resources.session_base.theory_qualifier(snapshot.node_name)
val chapter =
sessions.get(session) match {
--- a/src/Tools/jEdit/src/jedit_options.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala Fri Aug 12 20:21:09 2022 +0200
@@ -57,9 +57,9 @@
val button = new ColorWellButton(Color_Value(opt.value))
val component = new Component with Option_Component {
- override lazy val peer = button
+ override lazy val peer: JComponent = button
name = opt_name
- val title = opt_title
+ val title: String = opt_title
def load(): Unit = button.setSelectedColor(Color_Value(string(opt_name)))
def save(): Unit = string(opt_name) = Color_Value.print(button.getSelectedColor)
}
@@ -77,7 +77,7 @@
if (opt.typ == Options.Bool)
new CheckBox with Option_Component {
name = opt_name
- val title = opt_title
+ val title: String = opt_title
def load(): Unit = selected = bool(opt_name)
def save(): Unit = bool(opt_name) = selected
}
@@ -87,7 +87,7 @@
new TextArea with Option_Component {
if (default_font != null) font = default_font
name = opt_name
- val title = opt_title
+ val title: String = opt_title
def load(): Unit = text = value.check_name(opt_name).value
def save(): Unit =
try { JEdit_Options.this += (opt_name, text) }
@@ -97,14 +97,11 @@
GUI.scrollable_text(msg))
}
}
- text_area.peer.setInputVerifier(new InputVerifier {
- def verify(jcomponent: JComponent): Boolean =
- jcomponent match {
- case text: JTextComponent =>
- try { value + (opt_name, text.getText); true }
- catch { case ERROR(_) => false }
- case _ => true
- }
+ text_area.peer.setInputVerifier({
+ case text: JTextComponent =>
+ try { value + (opt_name, text.getText); true }
+ catch { case ERROR(_) => false }
+ case _ => true
})
GUI.plain_focus_traversal(text_area.peer)
text_area
--- a/src/Tools/jEdit/src/jedit_sessions.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Aug 12 20:21:09 2022 +0200
@@ -39,8 +39,12 @@
options2
}
- def sessions_structure(options: Options, dirs: List[Path] = session_dirs): Sessions.Structure =
+ 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 */
@@ -58,7 +62,7 @@
space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS"))
def logic_info(options: Options): Option[Sessions.Info] =
- try { sessions_structure(options).get(logic_name(options)) }
+ try { sessions_structure(options = options).get(logic_name(options)) }
catch { case ERROR(_) => None }
def logic_root(options: Options): Position.T =
@@ -68,26 +72,27 @@
/* 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 sessions = sessions_structure(options.value)
+ 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
- val component = new ComboBox(entries) with Option_Component {
+ 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)
@@ -97,15 +102,13 @@
}
}
def save(): Unit = options.string(jedit_logic_option) = selection.item.name
+
+ load()
+ if (autosave) {
+ listenTo(selection)
+ reactions += { case SelectionChanged(_) => save() }
+ }
}
-
- component.load()
- if (autosave) {
- component.listenTo(component.selection)
- component.reactions += { case SelectionChanged(_) => component.save() }
- }
- component.tooltip = "Logic session name (change requires restart)"
- component
}
--- a/src/Tools/jEdit/src/output_dockable.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Fri Aug 12 20:21:09 2022 +0200
@@ -33,12 +33,8 @@
override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
- private def handle_resize(): Unit = {
- GUI_Thread.require {}
-
- pretty_text_area.resize(
- Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
- }
+ private def handle_resize(): Unit =
+ GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit = {
GUI_Thread.require {}
@@ -96,7 +92,7 @@
reactions += { case ButtonClicked(_) => handle_update(true, None) }
}
- private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
private val controls =
Wrap_Panel(
--- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Aug 12 20:21:09 2022 +0200
@@ -122,6 +122,9 @@
refresh()
}
+ def zoom(factor: Int): Unit =
+ resize(Font_Info.main(PIDE.options.real("jedit_font_scale") * factor / 100))
+
def update(
base_snapshot: Document.Snapshot,
base_results: Command.Results,
@@ -136,13 +139,13 @@
refresh()
}
- def detach: Unit = {
+ def detach(): Unit = {
GUI_Thread.require {}
Info_Dockable(view, current_base_snapshot, current_base_results, current_body)
}
def detach_operation: Option[() => Unit] =
- if (current_body.isEmpty) None else Some(() => detach)
+ if (current_body.isEmpty) None else Some(() => detach())
/* common GUI components */
@@ -208,15 +211,15 @@
case KeyEvent.VK_C | KeyEvent.VK_INSERT
if strict_control && text_area.getSelectionCount != 0 =>
Registers.copy(text_area, '$')
- evt.consume
+ evt.consume()
case KeyEvent.VK_A
if strict_control =>
text_area.selectAll
- evt.consume
+ evt.consume()
case KeyEvent.VK_ESCAPE =>
- if (Isabelle.dismissed_popups(view)) evt.consume
+ if (Isabelle.dismissed_popups(view)) evt.consume()
case _ =>
}
--- a/src/Tools/jEdit/src/process_indicator.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/process_indicator.scala Fri Aug 12 20:21:09 2022 +0200
@@ -27,26 +27,24 @@
private class Animation extends ImageIcon(passive_icon) {
private var current_frame = 0
private val timer =
- new Timer(0, new ActionListener {
- override def actionPerformed(e: ActionEvent): Unit = {
- current_frame = (current_frame + 1) % active_icons.length
- setImage(active_icons(current_frame))
- label.repaint()
- }
+ new Timer(0, { (_: ActionEvent) =>
+ current_frame = (current_frame + 1) % active_icons.length
+ setImage(active_icons(current_frame))
+ label.repaint()
})
timer.setRepeats(true)
def update(rate: Int): Unit = {
if (rate == 0) {
setImage(passive_icon)
- timer.stop
+ timer.stop()
label.repaint()
}
else {
val delay = 1000 / rate
timer.setInitialDelay(delay)
timer.setDelay(delay)
- timer.restart
+ timer.restart()
}
}
}
--- a/src/Tools/jEdit/src/query_dockable.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Fri Aug 12 20:21:09 2022 +0200
@@ -24,7 +24,7 @@
val pretty_text_area = new Pretty_Text_Area(view)
def query_operation: Query_Operation[View]
def query: JComponent
- def select: Unit
+ def select(): Unit
def page: TabbedPane.Page
}
}
@@ -32,7 +32,7 @@
class Query_Dockable(view: View, position: String) extends Dockable(view, position) {
/* common GUI components */
- private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
private def make_query(
property: String,
@@ -71,7 +71,7 @@
/* find theorems */
- private val find_theorems = new Query_Dockable.Operation(view) {
+ private val find_theorems: Query_Dockable.Operation = new Query_Dockable.Operation(view) {
/* query */
private val process_indicator = new Process_Indicator
@@ -101,8 +101,7 @@
private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
tooltip = "Limit of displayed results"
- verifier = (s: String) =>
- s match { case Value.Int(x) => x >= 0 case _ => false }
+ verifier = { case Value.Int(x) => x >= 0 case _ => false }
listenTo(keys)
reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
}
@@ -124,7 +123,7 @@
process_indicator.component, apply_button,
pretty_text_area.search_label, pretty_text_area.search_field))
- def select: Unit = { control_panel.contents += zoom }
+ def select(): Unit = { control_panel.contents += zoom }
val page =
new TabbedPane.Page("Find Theorems", new BorderPanel {
@@ -136,7 +135,7 @@
/* find consts */
- private val find_consts = new Query_Dockable.Operation(view) {
+ private val find_consts: Query_Dockable.Operation = new Query_Dockable.Operation(view) {
/* query */
private val process_indicator = new Process_Indicator
@@ -173,7 +172,7 @@
query_label, Component.wrap(query), process_indicator.component, apply_button,
pretty_text_area.search_label, pretty_text_area.search_field))
- def select: Unit = { control_panel.contents += zoom }
+ def select(): Unit = { control_panel.contents += zoom }
val page =
new TabbedPane.Page("Find Constants", new BorderPanel {
@@ -189,7 +188,7 @@
/* items */
private class Item(val name: String, description: String, sel: Boolean) {
- val checkbox = new CheckBox(name) {
+ val checkbox: CheckBox = new CheckBox(name) {
tooltip = "Print " + description
selected = sel
reactions += { case ButtonClicked(_) => apply_query() }
@@ -243,14 +242,14 @@
reactions += {
case ButtonClicked(_) => apply_query()
case evt @ KeyPressed(_, Key.Enter, 0, _) =>
- evt.peer.consume
+ evt.peer.consume()
apply_query()
}
}
private val control_panel = Wrap_Panel()
- def select: Unit = {
+ def select(): Unit = {
control_panel.contents.clear()
control_panel.contents += query_label
update_items().foreach(item => control_panel.contents += item.checkbox)
@@ -282,7 +281,7 @@
catch { case _: IndexOutOfBoundsException => None }
private def select_operation(): Unit = {
- for (op <- get_operation()) { op.select; op.query.requestFocus() }
+ for (op <- get_operation()) { op.select(); op.query.requestFocus() }
operations_pane.revalidate()
}
@@ -303,12 +302,7 @@
/* resize */
private def handle_resize(): Unit =
- GUI_Thread.require {
- for (op <- operations) {
- op.pretty_text_area.resize(
- Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
- }
- }
+ GUI_Thread.require { operations.foreach(_.pretty_text_area.zoom(zoom.factor)) }
private val delay_resize =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Fri Aug 12 20:21:09 2022 +0200
@@ -133,7 +133,7 @@
GUI_Thread.require {}
private val pretty_text_area = new Pretty_Text_Area(view)
- private val zoom = new Font_Info.Zoom_Box { def changed = do_paint() }
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = do_paint() }
size = new Dimension(500, 500)
contents = new BorderPanel {
@@ -158,12 +158,8 @@
pretty_text_area.update(snapshot, Command.Results.empty, xml)
}
- def do_paint(): Unit = {
- GUI_Thread.later {
- pretty_text_area.resize(
- Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
- }
- }
+ def do_paint(): Unit =
+ GUI_Thread.later { pretty_text_area.zoom(zoom.factor) }
def handle_resize(): Unit = do_paint()
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Aug 12 20:21:09 2022 +0200
@@ -62,17 +62,13 @@
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
- private def handle_resize(): Unit = {
- GUI_Thread.require {}
-
- pretty_text_area.resize(
- Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
- }
+ private def handle_resize(): Unit =
+ GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
/* controls */
- private def clicked: Unit = {
+ private def clicked(): Unit = {
provers.addCurrentToHistory()
PIDE.options.string("sledgehammer_provers") = provers.getText
sledgehammer.apply_query(
@@ -88,7 +84,7 @@
private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {
override def processKeyEvent(evt: KeyEvent): Unit = {
- if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
+ if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked()
super.processKeyEvent(evt)
}
setToolTipText(provers_label.tooltip)
@@ -116,7 +112,7 @@
private val apply_query = new Button("<html><b>Apply</b></html>") {
tooltip = "Search for first-order proof using automatic theorem provers"
- reactions += { case ButtonClicked(_) => clicked }
+ reactions += { case ButtonClicked(_) => clicked() }
}
private val cancel_query = new Button("Cancel") {
@@ -129,7 +125,7 @@
reactions += { case ButtonClicked(_) => sledgehammer.locate_query() }
}
- private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
private val controls =
Wrap_Panel(
--- a/src/Tools/jEdit/src/state_dockable.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala Fri Aug 12 20:21:09 2022 +0200
@@ -45,12 +45,8 @@
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
- private def handle_resize(): Unit = {
- GUI_Thread.require {}
-
- pretty_text_area.resize(
- Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
- }
+ private def handle_resize(): Unit =
+ GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
/* update */
@@ -98,7 +94,7 @@
reactions += { case ButtonClicked(_) => print_state.locate_query() }
}
- private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
private val controls =
Wrap_Panel(
--- a/src/Tools/jEdit/src/theories_dockable.scala Fri Aug 12 15:35:07 2022 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Fri Aug 12 20:21:09 2022 +0200
@@ -83,7 +83,7 @@
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))