diff --git a/src/Pure/GUI/gui.scala b/src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala +++ b/src/Pure/GUI/gui.scala @@ -1,356 +1,357 @@ /* Title: Pure/GUI/gui.scala Author: Makarius Basic GUI tools (for AWT/Swing). */ package isabelle +import java.util.{Map => JMap} import java.awt.{Component, Container, Font, Image, Insets, KeyboardFocusManager, Window, Point, Rectangle, Dimension, GraphicsEnvironment, MouseInfo, Toolkit} import java.awt.font.{FontRenderContext, LineMetrics, TextAttribute, TransformAttribute} import java.awt.geom.AffineTransform import javax.swing.{ImageIcon, JButton, JDialog, JFrame, JLabel, JLayeredPane, JOptionPane, JTextField, JWindow, LookAndFeel, UIManager, SwingUtilities} import scala.swing.{ComboBox, ScrollPane, TextArea} import scala.swing.event.SelectionChanged object GUI { /* Swing look-and-feel */ def init_laf(): Unit = com.formdev.flatlaf.FlatLightLaf.setup() def current_laf: String = UIManager.getLookAndFeel.getClass.getName() def is_macos_laf: Boolean = Platform.is_macos && UIManager.getSystemLookAndFeelClassName() == current_laf class Look_And_Feel(laf: LookAndFeel) extends Isabelle_System.Service { def info: UIManager.LookAndFeelInfo = new UIManager.LookAndFeelInfo(laf.getName, laf.getClass.getName) } lazy val look_and_feels: List[Look_And_Feel] = Isabelle_System.make_services(classOf[Look_And_Feel]) def init_lafs(): Unit = { val old_lafs = Set( "com.sun.java.swing.plaf.motif.MotifLookAndFeel", "com.sun.java.swing.plaf.windows.WindowsClassicLookAndFeel") val lafs = UIManager.getInstalledLookAndFeels().toList .filterNot(info => old_lafs(info.getClassName)) val more_lafs = look_and_feels.map(_.info) UIManager.setInstalledLookAndFeels((more_lafs ::: lafs).toArray) } /* additional look-and-feels */ /* plain focus traversal, notably for text fields */ def plain_focus_traversal(component: Component): Unit = { val dummy_button = new JButton def apply(id: Int): Unit = component.setFocusTraversalKeys(id, dummy_button.getFocusTraversalKeys(id)) apply(KeyboardFocusManager.FORWARD_TRAVERSAL_KEYS) apply(KeyboardFocusManager.BACKWARD_TRAVERSAL_KEYS) } /* simple dialogs */ def scrollable_text(raw_txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false) : ScrollPane = { val txt = Output.clean_yxml(raw_txt) val text = new TextArea(txt) if (width > 0) text.columns = width if (height > 0 && split_lines(txt).length > height) text.rows = height text.editable = editable new ScrollPane(text) } private def simple_dialog(kind: Int, default_title: String, parent: Component, title: String, message: Iterable[Any]): Unit = { GUI_Thread.now { val java_message = message.iterator.map({ case x: scala.swing.Component => x.peer case x => x }). toArray.asInstanceOf[Array[AnyRef]] JOptionPane.showMessageDialog(parent, java_message, if (title == null) default_title else title, kind) } } def dialog(parent: Component, title: String, message: Any*): Unit = simple_dialog(JOptionPane.PLAIN_MESSAGE, null, parent, title, message) def warning_dialog(parent: Component, title: String, message: Any*): Unit = simple_dialog(JOptionPane.WARNING_MESSAGE, "Warning", parent, title, message) def error_dialog(parent: Component, title: String, message: Any*): Unit = simple_dialog(JOptionPane.ERROR_MESSAGE, "Error", parent, title, message) def confirm_dialog(parent: Component, title: String, option_type: Int, message: Any*): Int = GUI_Thread.now { val java_message = message map { case x: scala.swing.Component => x.peer case x => x } JOptionPane.showConfirmDialog(parent, java_message.toArray.asInstanceOf[Array[AnyRef]], title, option_type, JOptionPane.QUESTION_MESSAGE) } /* zoom box */ private val Zoom_Factor = "([0-9]+)%?".r abstract class Zoom_Box extends ComboBox[String]( List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%")) { def changed: Unit def factor: Int = parse(selection.item) private def parse(text: String): Int = text match { case Zoom_Factor(s) => val i = Integer.parseInt(s) if (10 <= i && i < 1000) i else 100 case _ => 100 } private def print(i: Int): String = i.toString + "%" def set_item(i: Int): Unit = { peer.getEditor match { case null => case editor => editor.setItem(print(i)) } } makeEditable()(c => new ComboBox.BuiltInEditor(c)(text => print(parse(text)), x => x)) peer.getEditor.getEditorComponent match { case text: JTextField => text.setColumns(4) case _ => } selection.index = 3 listenTo(selection) reactions += { case SelectionChanged(_) => changed } } /* tooltip with multi-line support */ def tooltip_lines(text: String): String = if (text == null || text == "") null else "" + HTML.output(text) + "" /* icon */ def isabelle_icon(): ImageIcon = new ImageIcon(getClass.getClassLoader.getResource("isabelle/isabelle_transparent-32.gif")) def isabelle_icons(): List[ImageIcon] = for (icon <- List("isabelle/isabelle_transparent-32.gif", "isabelle/isabelle_transparent.gif")) yield new ImageIcon(getClass.getClassLoader.getResource(icon)) def isabelle_image(): Image = isabelle_icon().getImage /* location within multi-screen environment */ final case class Screen_Location(point: Point, bounds: Rectangle) { def relative(parent: Component, size: Dimension): Point = { val w = size.width val h = size.height val x0 = parent.getLocationOnScreen.x val y0 = parent.getLocationOnScreen.y val x1 = x0 + parent.getWidth - w val y1 = y0 + parent.getHeight - h val x2 = point.x min (bounds.x + bounds.width - w) val y2 = point.y min (bounds.y + bounds.height - h) val location = new Point((x2 min x1) max x0, (y2 min y1) max y0) SwingUtilities.convertPointFromScreen(location, parent) location } } def screen_location(component: Component, point: Point): Screen_Location = { val screen_point = new Point(point.x, point.y) if (component != null) SwingUtilities.convertPointToScreen(screen_point, component) val ge = GraphicsEnvironment.getLocalGraphicsEnvironment val screen_bounds = (for { device <- ge.getScreenDevices.iterator config <- device.getConfigurations.iterator bounds = config.getBounds } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds Screen_Location(screen_point, screen_bounds) } def mouse_location(): Screen_Location = screen_location(null, MouseInfo.getPointerInfo.getLocation) /* screen size */ sealed case class Screen_Size(bounds: Rectangle, insets: Insets) { def full_screen_bounds: Rectangle = if (Platform.is_linux) { // avoid menu bar and docking areas new Rectangle( bounds.x + insets.left, bounds.y + insets.top, bounds.width - insets.left - insets.right, bounds.height - insets.top - insets.bottom) } else if (Platform.is_macos) { // avoid menu bar, but ignore docking areas new Rectangle( bounds.x, bounds.y + insets.top, bounds.width, bounds.height - insets.top) } else bounds } def screen_size(component: Component): Screen_Size = { val config = component.getGraphicsConfiguration val bounds = config.getBounds val insets = Toolkit.getDefaultToolkit.getScreenInsets(config) Screen_Size(bounds, insets) } /* component hierachy */ def get_parent(component: Component): Option[Container] = component.getParent match { case null => None case parent => Some(parent) } def ancestors(component: Component): Iterator[Container] = new Iterator[Container] { private var next_elem = get_parent(component) def hasNext: Boolean = next_elem.isDefined def next(): Container = next_elem match { case Some(parent) => next_elem = get_parent(parent) parent case None => Iterator.empty.next() } } def parent_window(component: Component): Option[Window] = ancestors(component).collectFirst({ case x: Window => x }) def layered_pane(component: Component): Option[JLayeredPane] = parent_window(component) match { case Some(w: JWindow) => Some(w.getLayeredPane) case Some(w: JFrame) => Some(w.getLayeredPane) case Some(w: JDialog) => Some(w.getLayeredPane) case _ => None } def traverse_components(component: Component, apply: Component => Unit): Unit = { def traverse(comp: Component): Unit = { apply(comp) comp match { case cont: Container => for (i <- 0 until cont.getComponentCount) traverse(cont.getComponent(i)) case _ => } } traverse(component) } /* font operations */ def copy_font(font: Font): Font = if (font == null) null else new Font(font.getFamily, font.getStyle, font.getSize) def line_metrics(font: Font): LineMetrics = font.getLineMetrics("", new FontRenderContext(null, false, false)) def transform_font(font: Font, transform: AffineTransform): Font = - font.deriveFont(java.util.Map.of(TextAttribute.TRANSFORM, new TransformAttribute(transform))) + font.deriveFont(JMap.of(TextAttribute.TRANSFORM, new TransformAttribute(transform))) def font(family: String = Isabelle_Fonts.sans, size: Int = 1, bold: Boolean = false): Font = new Font(family, if (bold) Font.BOLD else Font.PLAIN, size) def label_font(): Font = (new JLabel).getFont /* Isabelle fonts */ def imitate_font(font: Font, family: String = Isabelle_Fonts.sans, scale: Double = 1.0): Font = { val font1 = new Font(family, font.getStyle, font.getSize) val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight new Font(family, font.getStyle, (scale * rel_size * font.getSize).toInt) } def imitate_font_css(font: Font, family: String = Isabelle_Fonts.sans, scale: Double = 1.0): String = { val font1 = new Font(family, font.getStyle, font.getSize) val rel_size = line_metrics(font).getHeight.toDouble / line_metrics(font1).getHeight "font-family: " + family + "; font-size: " + (scale * rel_size * 100).toInt + "%;" } def use_isabelle_fonts(): Unit = { val default_font = label_font() val ui = UIManager.getDefaults for (prop <- List( "ToggleButton.font", "CheckBoxMenuItem.font", "Label.font", "Menu.font", "MenuItem.font", "PopupMenu.font", "Table.font", "TableHeader.font", "TextArea.font", "TextField.font", "TextPane.font", "ToolTip.font", "Tree.font")) { val font = ui.get(prop) match { case font: Font => font case _ => default_font } ui.put(prop, GUI.imitate_font(font)) } } } class FlatLightLaf extends GUI.Look_And_Feel(new com.formdev.flatlaf.FlatLightLaf) class FlatDarkLaf extends GUI.Look_And_Feel(new com.formdev.flatlaf.FlatDarkLaf) diff --git a/src/Pure/General/file_watcher.scala b/src/Pure/General/file_watcher.scala --- a/src/Pure/General/file_watcher.scala +++ b/src/Pure/General/file_watcher.scala @@ -1,135 +1,136 @@ /* Title: Pure/General/file_watcher.scala Author: Makarius Watcher for file-system events. */ package isabelle +import java.util.{List => JList} import java.io.{File => JFile} import java.nio.file.FileSystems import java.nio.file.{WatchKey, WatchEvent, Path => JPath} import java.nio.file.StandardWatchEventKinds.{ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY} import scala.jdk.CollectionConverters._ class File_Watcher private[File_Watcher] // dummy template { def register(dir: JFile): Unit = {} def register_parent(file: JFile): Unit = {} def deregister(dir: JFile): Unit = {} def purge(retain: Set[JFile]): Unit = {} def shutdown(): Unit = {} } object File_Watcher { val none: File_Watcher = new File_Watcher { override def toString: String = "File_Watcher.none" } def apply(handle: Set[JFile] => Unit, delay: => Time = Time.seconds(0.5)): File_Watcher = if (Platform.is_windows) none else new Impl(handle, delay) /* proper implementation */ sealed case class State( dirs: Map[JFile, WatchKey] = Map.empty, changed: Set[JFile] = Set.empty) class Impl private[File_Watcher](handle: Set[JFile] => Unit, delay: Time) extends File_Watcher { private val state = Synchronized(File_Watcher.State()) private val watcher = FileSystems.getDefault.newWatchService() override def toString: String = state.value.dirs.keySet.mkString("File_Watcher(", ", ", ")") /* registered directories */ override def register(dir: JFile): Unit = state.change(st => st.dirs.get(dir) match { case Some(key) if key.isValid => st case _ => val key = dir.toPath.register(watcher, ENTRY_CREATE, ENTRY_DELETE, ENTRY_MODIFY) st.copy(dirs = st.dirs + (dir -> key)) }) override def register_parent(file: JFile): Unit = { val dir = file.getParentFile if (dir != null && dir.isDirectory) register(dir) } override def deregister(dir: JFile): Unit = state.change(st => st.dirs.get(dir) match { case None => st case Some(key) => key.cancel() st.copy(dirs = st.dirs - dir) }) override def purge(retain: Set[JFile]): Unit = state.change(st => st.copy(dirs = st.dirs -- (for ((dir, key) <- st.dirs.iterator if !retain(dir)) yield { key.cancel(); dir }))) /* changed directory entries */ private val delay_changed = Delay.last(delay) { val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty))) handle(changed) } private val watcher_thread = Isabelle_Thread.fork(name = "file_watcher", daemon = true) { try { while (true) { val key = watcher.take val has_changed = state.change_result(st => { val (remove, changed) = st.dirs.collectFirst({ case (dir, key1) if key == key1 => dir }) match { case Some(dir) => val events: Iterable[WatchEvent[JPath]] = - key.pollEvents.asInstanceOf[java.util.List[WatchEvent[JPath]]].asScala + key.pollEvents.asInstanceOf[JList[WatchEvent[JPath]]].asScala val remove = if (key.reset) None else Some(dir) val changed = events.iterator.foldLeft(Set.empty[JFile]) { case (set, event) => set + dir.toPath.resolve(event.context).toFile } (remove, changed) case None => key.pollEvents key.reset (None, Set.empty[JFile]) } (changed.nonEmpty, st.copy(dirs = st.dirs -- remove, changed = st.changed ++ changed)) }) if (has_changed) delay_changed.invoke() } } catch { case Exn.Interrupt() => } } /* shutdown */ override def shutdown(): Unit = { watcher_thread.interrupt() watcher_thread.join delay_changed.revoke() } } } diff --git a/src/Pure/General/ssh.scala b/src/Pure/General/ssh.scala --- a/src/Pure/General/ssh.scala +++ b/src/Pure/General/ssh.scala @@ -1,524 +1,524 @@ /* Title: Pure/General/ssh.scala Author: Makarius SSH client based on JSch (see also http://www.jcraft.com/jsch/examples). */ package isabelle -import java.util.{Map => JMap, HashMap} +import java.util.{Map => JMap} import java.io.{InputStream, OutputStream, ByteArrayOutputStream} import scala.collection.mutable import scala.util.matching.Regex import com.jcraft.jsch.{JSch, Logger => JSch_Logger, Session => JSch_Session, SftpException, OpenSSHConfig, UserInfo, Channel => JSch_Channel, ChannelExec, ChannelSftp, SftpATTRS, JSchException} object SSH { /* target machine: user@host syntax */ object Target { val User_Host: Regex = "^([^@]+)@(.+)$".r def parse(s: String): (String, String) = s match { case User_Host(user, host) => (user, host) case _ => ("", s) } def unapplySeq(s: String): Option[List[String]] = parse(s) match { case (_, "") => None case (user, host) => Some(List(user, host)) } } val default_port = 22 def make_port(port: Int): Int = if (port > 0) port else default_port def port_suffix(port: Int): String = if (port == default_port) "" else ":" + port def user_prefix(user: String): String = proper_string(user) match { case None => "" case Some(name) => name + "@" } def connect_timeout(options: Options): Int = options.seconds("ssh_connect_timeout").ms.toInt def alive_interval(options: Options): Int = options.seconds("ssh_alive_interval").ms.toInt def alive_count_max(options: Options): Int = options.int("ssh_alive_count_max") /* init context */ def init_context(options: Options): Context = { val config_dir = Path.explode(options.string("ssh_config_dir")) if (!config_dir.is_dir) error("Bad ssh config directory: " + config_dir) val jsch = new JSch val config_file = Path.explode(options.string("ssh_config_file")) if (config_file.is_file) jsch.setConfigRepository(OpenSSHConfig.parseFile(File.platform_path(config_file))) val known_hosts = config_dir + Path.explode("known_hosts") if (!known_hosts.is_file) known_hosts.file.createNewFile jsch.setKnownHosts(File.platform_path(known_hosts)) val identity_files = space_explode(':', options.string("ssh_identity_files")).map(Path.explode) for (identity_file <- identity_files if identity_file.is_file) { try { jsch.addIdentity(File.platform_path(identity_file)) } catch { case exn: JSchException => error("Error in ssh identity file " + identity_file + ": " + exn.getMessage) } } new Context(options, jsch) } def open_session(options: Options, host: String, user: String = "", port: Int = 0, actual_host: String = "", proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, permissive: Boolean = false): Session = init_context(options).open_session( host = host, user = user, port = port, actual_host = actual_host, proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port, permissive = permissive) class Context private[SSH](val options: Options, val jsch: JSch) { def update_options(new_options: Options): Context = new Context(new_options, jsch) private def connect_session(host: String, user: String = "", port: Int = 0, host_key_permissive: Boolean = false, nominal_host: String = "", nominal_user: String = "", on_close: () => Unit = () => ()): Session = { val session = jsch.getSession(proper_string(user).orNull, host, make_port(port)) session.setUserInfo(No_User_Info) session.setServerAliveInterval(alive_interval(options)) session.setServerAliveCountMax(alive_count_max(options)) session.setConfig("MaxAuthTries", "3") if (host_key_permissive) session.setConfig("StrictHostKeyChecking", "no") if (nominal_host != "") session.setHostKeyAlias(nominal_host) if (options.bool("ssh_compression")) { session.setConfig("compression.s2c", "zlib@openssh.com,zlib,none") session.setConfig("compression.c2s", "zlib@openssh.com,zlib,none") session.setConfig("compression_level", "9") } session.connect(connect_timeout(options)) new Session(options, session, on_close, proper_string(nominal_host) getOrElse host, proper_string(nominal_user) getOrElse user) } def open_session( host: String, user: String = "", port: Int = 0, actual_host: String = "", proxy_host: String = "", proxy_user: String = "", proxy_port: Int = 0, permissive: Boolean = false): Session = { val connect_host = proper_string(actual_host) getOrElse host if (proxy_host == "") connect_session(host = connect_host, user = user, port = port) else { val proxy = connect_session(host = proxy_host, port = proxy_port, user = proxy_user) val fw = try { proxy.port_forwarding(remote_host = connect_host, remote_port = make_port(port)) } catch { case exn: Throwable => proxy.close(); throw exn } try { connect_session(host = fw.local_host, port = fw.local_port, host_key_permissive = permissive, nominal_host = host, nominal_user = user, user = user, on_close = () => { fw.close(); proxy.close() }) } catch { case exn: Throwable => fw.close(); proxy.close(); throw exn } } } } /* logging */ def logging(verbose: Boolean = true, debug: Boolean = false): Unit = { JSch.setLogger(if (verbose) new Logger(debug) else null) } private class Logger(debug: Boolean) extends JSch_Logger { def isEnabled(level: Int): Boolean = level != JSch_Logger.DEBUG || debug def log(level: Int, msg: String): Unit = { level match { case JSch_Logger.ERROR | JSch_Logger.FATAL => Output.error_message(msg) case JSch_Logger.WARN => Output.warning(msg) case _ => Output.writeln(msg) } } } /* user info */ object No_User_Info extends UserInfo { def getPassphrase: String = null def getPassword: String = null def promptPassword(msg: String): Boolean = false def promptPassphrase(msg: String): Boolean = false def promptYesNo(msg: String): Boolean = false def showMessage(msg: String): Unit = Output.writeln(msg) } /* port forwarding */ object Port_Forwarding { def open(ssh: Session, ssh_close: Boolean, local_host: String, local_port: Int, remote_host: String, remote_port: Int): Port_Forwarding = { val port = ssh.session.setPortForwardingL(local_host, local_port, remote_host, remote_port) new Port_Forwarding(ssh, ssh_close, local_host, port, remote_host, remote_port) } } class Port_Forwarding private[SSH]( ssh: SSH.Session, ssh_close: Boolean, val local_host: String, val local_port: Int, val remote_host: String, val remote_port: Int) extends AutoCloseable { override def toString: String = local_host + ":" + local_port + ":" + remote_host + ":" + remote_port def close(): Unit = { ssh.session.delPortForwardingL(local_host, local_port) if (ssh_close) ssh.close() } } /* Sftp channel */ type Attrs = SftpATTRS sealed case class Dir_Entry(name: String, is_dir: Boolean) { def is_file: Boolean = !is_dir } /* exec channel */ private val exec_wait_delay = Time.seconds(0.3) class Exec private[SSH](session: Session, channel: ChannelExec) extends AutoCloseable { override def toString: String = "exec " + session.toString def close(): Unit = channel.disconnect val exit_status: Future[Int] = Future.thread("ssh_wait") { while (!channel.isClosed) exec_wait_delay.sleep() channel.getExitStatus } val stdin: OutputStream = channel.getOutputStream val stdout: InputStream = channel.getInputStream val stderr: InputStream = channel.getErrStream // connect after preparing streams channel.connect(connect_timeout(session.options)) def result( progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), strict: Boolean = true): Process_Result = { stdin.close() def read_lines(stream: InputStream, progress: String => Unit): List[String] = { val result = new mutable.ListBuffer[String] val line_buffer = new ByteArrayOutputStream(100) def line_flush(): Unit = { val line = Library.trim_line(line_buffer.toString(UTF8.charset_name)) progress(line) result += line line_buffer.reset } var c = 0 var finished = false while (!finished) { while ({ c = stream.read; c != -1 && c != 10 }) line_buffer.write(c) if (c == 10) line_flush() else if (channel.isClosed) { if (line_buffer.size > 0) line_flush() finished = true } else exec_wait_delay.sleep() } result.toList } val out_lines = Future.thread("ssh_stdout") { read_lines(stdout, progress_stdout) } val err_lines = Future.thread("ssh_stderr") { read_lines(stderr, progress_stderr) } def terminate(): Unit = { close() out_lines.join err_lines.join exit_status.join } val rc = try { exit_status.join } catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code } close() if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() Process_Result(rc, out_lines.join, err_lines.join) } } /* session */ class Session private[SSH]( val options: Options, val session: JSch_Session, on_close: () => Unit, val nominal_host: String, val nominal_user: String) extends System { def update_options(new_options: Options): Session = new Session(new_options, session, on_close, nominal_host, nominal_user) def host: String = if (session.getHost == null) "" else session.getHost override def hg_url: String = "ssh://" + user_prefix(nominal_user) + nominal_host + "/" override def toString: String = user_prefix(session.getUserName) + host + port_suffix(session.getPort) + (if (session.isConnected) "" else " (disconnected)") /* port forwarding */ def port_forwarding( remote_port: Int, remote_host: String = "localhost", local_port: Int = 0, local_host: String = "localhost", ssh_close: Boolean = false): Port_Forwarding = Port_Forwarding.open(this, ssh_close, local_host, local_port, remote_host, remote_port) /* sftp channel */ val sftp: ChannelSftp = session.openChannel("sftp").asInstanceOf[ChannelSftp] sftp.connect(connect_timeout(options)) override def close(): Unit = { sftp.disconnect; session.disconnect; on_close() } val settings: JMap[String, String] = { val home = sftp.getHome JMap.of("HOME", home, "USER_HOME", home) } override def expand_path(path: Path): Path = path.expand_env(settings) def remote_path(path: Path): String = expand_path(path).implode override def bash_path(path: Path): String = Bash.string(remote_path(path)) def chmod(permissions: Int, path: Path): Unit = sftp.chmod(permissions, remote_path(path)) def mv(path1: Path, path2: Path): Unit = sftp.rename(remote_path(path1), remote_path(path2)) def rm(path: Path): Unit = sftp.rm(remote_path(path)) def mkdir(path: Path): Unit = sftp.mkdir(remote_path(path)) def rmdir(path: Path): Unit = sftp.rmdir(remote_path(path)) private def test_entry(path: Path, as_dir: Boolean): Boolean = try { val is_dir = sftp.stat(remote_path(path)).isDir if (as_dir) is_dir else !is_dir } catch { case _: SftpException => false } override def is_dir(path: Path): Boolean = test_entry(path, true) override def is_file(path: Path): Boolean = test_entry(path, false) def is_link(path: Path): Boolean = try { sftp.lstat(remote_path(path)).isLink } catch { case _: SftpException => false } override def make_directory(path: Path): Path = { if (!is_dir(path)) { execute( "perl -e \"use File::Path make_path; make_path('" + remote_path(path) + "');\"") if (!is_dir(path)) error("Failed to create directory: " + quote(remote_path(path))) } path } def read_dir(path: Path): List[Dir_Entry] = { if (!is_dir(path)) error("No such directory: " + path.toString) val dir_name = remote_path(path) val dir = sftp.ls(dir_name) (for { i <- (0 until dir.size).iterator a = dir.get(i).asInstanceOf[AnyRef] name = Untyped.get[String](a, "filename") attrs = Untyped.get[Attrs](a, "attrs") if name != "." && name != ".." } yield { Dir_Entry(name, if (attrs.isLink) { try { sftp.stat(dir_name + "/" + name).isDir } catch { case _: SftpException => false } } else attrs.isDir) }).toList.sortBy(_.name) } def find_files( start: Path, pred: Path => Boolean = _ => true, include_dirs: Boolean = false, follow_links: Boolean = false): List[Path] = { val result = new mutable.ListBuffer[Path] def check(path: Path): Unit = { if (pred(path)) result += path } def find(dir: Path): Unit = { if (include_dirs) check(dir) if (follow_links || !is_link(dir)) { for (entry <- read_dir(dir)) { val path = dir + Path.basic(entry.name) if (entry.is_file) check(path) else find(path) } } } if (is_file(start)) check(start) else find(start) result.toList } def open_input(path: Path): InputStream = sftp.get(remote_path(path)) def open_output(path: Path): OutputStream = sftp.put(remote_path(path)) override def read_file(path: Path, local_path: Path): Unit = sftp.get(remote_path(path), File.platform_path(local_path)) def read_bytes(path: Path): Bytes = using(open_input(path))(Bytes.read_stream(_)) def read(path: Path): String = using(open_input(path))(File.read_stream) override def write_file(path: Path, local_path: Path): Unit = sftp.put(File.platform_path(local_path), remote_path(path)) def write_bytes(path: Path, bytes: Bytes): Unit = using(open_output(path))(bytes.write_stream) def write(path: Path, text: String): Unit = using(open_output(path))(stream => Bytes(text).write_stream(stream)) /* exec channel */ def exec(command: String): Exec = { val channel = session.openChannel("exec").asInstanceOf[ChannelExec] channel.setCommand("export USER_HOME=\"$HOME\"\n" + command) new Exec(this, channel) } override def execute(command: String, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), settings: Boolean = true, strict: Boolean = true): Process_Result = exec(command).result(progress_stdout, progress_stderr, strict) override def isabelle_platform: Isabelle_Platform = Isabelle_Platform(ssh = Some(this)) /* tmp dirs */ def rm_tree(dir: Path): Unit = rm_tree(remote_path(dir)) def rm_tree(remote_dir: String): Unit = execute("rm -r -f " + Bash.string(remote_dir)).check def tmp_dir(): String = execute("mktemp -d -t tmp.XXXXXXXXXX").check.out override def with_tmp_dir[A](body: Path => A): A = { val remote_dir = tmp_dir() try { body(Path.explode(remote_dir)) } finally { rm_tree(remote_dir) } } } /* system operations */ trait System extends AutoCloseable { def close(): Unit = () def hg_url: String = "" def expand_path(path: Path): Path = path.expand def bash_path(path: Path): String = File.bash_path(path) def is_dir(path: Path): Boolean = path.is_dir def is_file(path: Path): Boolean = path.is_file def make_directory(path: Path): Path = Isabelle_System.make_directory(path) def with_tmp_dir[A](body: Path => A): A = Isabelle_System.with_tmp_dir("tmp")(body) def read_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path1, path2) def write_file(path1: Path, path2: Path): Unit = Isabelle_System.copy_file(path2, path1) def execute(command: String, progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), settings: Boolean = true, strict: Boolean = true): Process_Result = Isabelle_System.bash(command, progress_stdout = progress_stdout, progress_stderr = progress_stderr, env = if (settings) Isabelle_System.settings() else null, strict = strict) def isabelle_platform: Isabelle_Platform = Isabelle_Platform() } object Local extends System } diff --git a/src/Pure/System/isabelle_charset.scala b/src/Pure/System/isabelle_charset.scala --- a/src/Pure/System/isabelle_charset.scala +++ b/src/Pure/System/isabelle_charset.scala @@ -1,50 +1,51 @@ /* Title: Pure/System/isabelle_charset.scala Author: Makarius Charset for Isabelle symbols. */ package isabelle +import java.util.{List => JList} import java.nio.Buffer import java.nio.{ByteBuffer, CharBuffer} import java.nio.charset.{Charset, CharsetDecoder, CharsetEncoder, CoderResult} import java.nio.charset.spi.CharsetProvider object Isabelle_Charset { val name: String = "UTF-8-Isabelle-test" // FIXME lazy val charset: Charset = new Isabelle_Charset } class Isabelle_Charset extends Charset(Isabelle_Charset.name, null) { override def contains(cs: Charset): Boolean = cs.name.equalsIgnoreCase(UTF8.charset_name) || UTF8.charset.contains(cs) override def newDecoder(): CharsetDecoder = UTF8.charset.newDecoder override def newEncoder(): CharsetEncoder = UTF8.charset.newEncoder } class Isabelle_Charset_Provider extends CharsetProvider { override def charsetForName(name: String): Charset = { // FIXME inactive // if (name.equalsIgnoreCase(Isabelle_Charset.name)) Isabelle_Charset.charset // else null null } override def charsets(): java.util.Iterator[Charset] = { // FIXME inactive // Iterator(Isabelle_Charset.charset) - java.util.List.of[Charset]().listIterator() + JList.of[Charset]().listIterator() } } diff --git a/src/Pure/Tools/spell_checker.scala b/src/Pure/Tools/spell_checker.scala --- a/src/Pure/Tools/spell_checker.scala +++ b/src/Pure/Tools/spell_checker.scala @@ -1,289 +1,290 @@ /* Title: Pure/Tools/spell_checker.scala Author: Makarius Spell checker with completion, based on JOrtho (see https://sourceforge.net/projects/jortho). */ package isabelle import java.lang.Class +import java.util.{List => JList} import scala.collection.mutable import scala.annotation.tailrec import scala.collection.immutable.SortedMap object Spell_Checker { /* words within text */ def marked_words(base: Text.Offset, text: String, mark: Text.Info[String] => Boolean) : List[Text.Info[String]] = { val result = new mutable.ListBuffer[Text.Info[String]] var offset = 0 def apostrophe(c: Int): Boolean = c == '\'' && (offset + 1 == text.length || text(offset + 1) != '\'') @tailrec def scan(pred: Int => Boolean): Unit = { if (offset < text.length) { val c = text.codePointAt(offset) if (pred(c)) { offset += Character.charCount(c) scan(pred) } } } while (offset < text.length) { scan(c => !Character.isLetter(c)) val start = offset scan(c => Character.isLetterOrDigit(c) || apostrophe(c)) val stop = offset if (stop - start >= 2) { val info = Text.Info(Text.Range(base + start, base + stop), text.substring(start, stop)) if (mark(info)) result += info } } result.toList } def current_word(rendering: Rendering, range: Text.Range): Option[Text.Info[String]] = { for { spell_range <- rendering.spell_checker_point(range) text <- rendering.get_text(spell_range) info <- marked_words(spell_range.start, text, info => info.range.overlaps(range)).headOption } yield info } /* dictionaries */ class Dictionary private[Spell_Checker](val path: Path) { val lang: String = path.drop_ext.file_name val user_path: Path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang) override def toString: String = lang } private object Decl { def apply(name: String, include: Boolean): String = if (include) name else "-" + name def unapply(decl: String): Option[(String, Boolean)] = { val decl1 = decl.trim if (decl1 == "" || decl1.startsWith("#")) None else Library.try_unprefix("-", decl1.trim) match { case None => Some((decl1, true)) case Some(decl2) => Some((decl2, false)) } } } def dictionaries: List[Dictionary] = for { path <- Path.split(Isabelle_System.getenv("JORTHO_DICTIONARIES")) if path.is_file } yield new Dictionary(path) /* create spell checker */ def apply(dictionary: Dictionary): Spell_Checker = new Spell_Checker(dictionary) private sealed case class Update(include: Boolean, permanent: Boolean) } class Spell_Checker private(dictionary: Spell_Checker.Dictionary) { override def toString: String = dictionary.toString /* main dictionary content */ private var dict = new Object private var updates = SortedMap.empty[String, Spell_Checker.Update] private def included_iterator(): Iterator[String] = for { (word, upd) <- updates.iterator if upd.include } yield word private def excluded(word: String): Boolean = updates.get(word) match { case Some(upd) => !upd.include case None => false } private def load(): Unit = { val main_dictionary = split_lines(File.read_gzip(dictionary.path)) val permanent_updates = if (dictionary.user_path.is_file) for { Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path)) } yield (word, Spell_Checker.Update(include, true)) else Nil updates = updates -- (for ((name, upd) <- updates.iterator; if upd.permanent) yield name) ++ permanent_updates val factory_class = Class.forName("com.inet.jortho.DictionaryFactory") val factory = Untyped.constructor(factory_class).newInstance() val add = Untyped.method(factory_class, "add", classOf[String]) for { word <- main_dictionary.iterator ++ included_iterator() if !excluded(word) } add.invoke(factory, word) dict = Untyped.method(factory_class, "create").invoke(factory) } load() private def save(): Unit = { val permanent_decls = (for { (word, upd) <- updates.iterator if upd.permanent } yield Spell_Checker.Decl(word, upd.include)).toList if (permanent_decls.nonEmpty || dictionary.user_path.is_file) { val header = """# User updates for spell-checker dictionary # # * each line contains at most one word # * extra blanks are ignored # * lines starting with "#" are stripped # * lines starting with "-" indicate excluded words # #:mode=text:encoding=UTF-8: """ Isabelle_System.make_directory(dictionary.user_path.expand.dir) File.write(dictionary.user_path, header + cat_lines(permanent_decls)) } } def update(word: String, include: Boolean, permanent: Boolean): Unit = { updates += (word -> Spell_Checker.Update(include, permanent)) if (include) { if (permanent) save() Untyped.method(dict.getClass, "add", classOf[String]).invoke(dict, word) } else { save(); load() } } def reset(): Unit = { updates = SortedMap.empty load() } def reset_enabled(): Int = updates.valuesIterator.count(upd => !upd.permanent) /* check known words */ def contains(word: String): Boolean = Untyped.method(dict.getClass.getSuperclass, "exist", classOf[String]). invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue def check(word: String): Boolean = word match { case Word.Case(c) if c != Word.Lowercase => contains(word) || contains(Word.lowercase(word)) case _ => contains(word) } def marked_words(base: Text.Offset, text: String): List[Text.Info[String]] = Spell_Checker.marked_words(base, text, info => !check(info.info)) /* completion: suggestions for unknown words */ private def suggestions(word: String): Option[List[String]] = { val res = Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]). - invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString) + invoke(dict, word).asInstanceOf[JList[AnyRef]].toArray.toList.map(_.toString) if (res.isEmpty) None else Some(res) } def complete(word: String): List[String] = if (check(word)) Nil else { val word_case = Word.Case.unapply(word) def recover_case(s: String) = word_case match { case Some(c) => Word.Case(c, s) case None => s } val result = word_case match { case Some(c) if c != Word.Lowercase => suggestions(word) orElse suggestions(Word.lowercase(word)) case _ => suggestions(word) } result.getOrElse(Nil).map(recover_case) } def completion(rendering: Rendering, caret: Text.Offset): Option[Completion.Result] = { val caret_range = rendering.before_caret_range(caret) for { word <- Spell_Checker.current_word(rendering, caret_range) words = complete(word.info) if words.nonEmpty descr = "(from dictionary " + quote(dictionary.toString) + ")" items = words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false)) } yield Completion.Result(word.range, word.info, false, items) } } class Spell_Checker_Variable { private val no_spell_checker: (String, Option[Spell_Checker]) = ("", None) private var current_spell_checker = no_spell_checker def get: Option[Spell_Checker] = synchronized { current_spell_checker._2 } def update(options: Options): Unit = synchronized { if (options.bool("spell_checker")) { val lang = options.string("spell_checker_dictionary") if (current_spell_checker._1 != lang) { Spell_Checker.dictionaries.find(_.lang == lang) match { case Some(dictionary) => val spell_checker = Exn.capture { Spell_Checker(dictionary) } match { case Exn.Res(spell_checker) => Some(spell_checker) case Exn.Exn(_) => None } current_spell_checker = (lang, spell_checker) case None => current_spell_checker = no_spell_checker } } } else current_spell_checker = no_spell_checker } } diff --git a/src/Tools/Graphview/metrics.scala b/src/Tools/Graphview/metrics.scala --- a/src/Tools/Graphview/metrics.scala +++ b/src/Tools/Graphview/metrics.scala @@ -1,64 +1,65 @@ /* Title: Tools/Graphview/metrics.scala Author: Makarius Physical metrics for layout and painting. */ package isabelle.graphview import isabelle._ +import java.util.HashMap import java.awt.{Font, RenderingHints} import java.awt.font.FontRenderContext import java.awt.geom.Rectangle2D object Metrics { val rendering_hints: RenderingHints = { - val hints = new java.util.HashMap[RenderingHints.Key, AnyRef] + val hints = new HashMap[RenderingHints.Key, AnyRef] hints.put(RenderingHints.KEY_ANTIALIASING, RenderingHints.VALUE_ANTIALIAS_ON) hints.put(RenderingHints.KEY_FRACTIONALMETRICS, RenderingHints.VALUE_FRACTIONALMETRICS_ON) new RenderingHints(hints) } val font_render_context: FontRenderContext = new FontRenderContext(null, true, true) def apply(font: Font): Metrics = new Metrics(font) val default: Metrics = apply(new Font("Helvetica", Font.PLAIN, 12)) } class Metrics private(val font: Font) { def string_bounds(s: String): Rectangle2D = font.getStringBounds(s, Metrics.font_render_context) private val mix = string_bounds("mix") val space_width: Double = string_bounds(" ").getWidth def char_width: Double = mix.getWidth / 3 def height: Double = mix.getHeight def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent def gap: Double = mix.getWidth.ceil def dummy_size2: Double = (char_width / 2).ceil def node_width2(lines: List[String]): Double = ((lines.foldLeft(0.0)({ case (w, s) => w max string_bounds(s).getWidth }) + 2 * char_width) / 2) .ceil def node_height2(num_lines: Int): Double = ((height.ceil * (num_lines max 1) + char_width) / 2).ceil def level_height2(num_lines: Int, num_edges: Int): Double = (node_height2(num_lines) + gap) max (node_height2(1) * (num_edges max 5)) object Pretty_Metric extends Pretty.Metric { val unit: Double = space_width max 1.0 def apply(s: String): Double = if (s == "\n") 1.0 else string_bounds(s).getWidth / unit } } diff --git a/src/Tools/jEdit/src-base/pide_docking_framework.scala b/src/Tools/jEdit/src-base/pide_docking_framework.scala --- a/src/Tools/jEdit/src-base/pide_docking_framework.scala +++ b/src/Tools/jEdit/src-base/pide_docking_framework.scala @@ -1,71 +1,72 @@ /* Title: Tools/jEdit/src-base/pide_docking_framework.scala Author: Makarius PIDE docking framework: "Original" with some add-ons. */ package isabelle.jedit_base import isabelle._ +import java.util.{List => JList} import java.awt.event.{ActionListener, ActionEvent} import javax.swing.{JPopupMenu, JMenuItem} import org.gjt.sp.jedit.View import org.gjt.sp.jedit.gui.{DockableWindowManagerProvider, DockableWindowFactory, DockableWindowManager, DockableWindowManagerImpl, DockableWindowContainer, FloatingWindowContainer, PanelWindowContainer} class PIDE_Docking_Framework extends DockableWindowManagerProvider { override def create( view: View, instance: DockableWindowFactory, config: View.ViewConfig): DockableWindowManager = new DockableWindowManagerImpl(view, instance, config) { override def createPopupMenu( container: DockableWindowContainer, dockable_name: String, clone: Boolean): JPopupMenu = { val menu = super.createPopupMenu(container, dockable_name, clone) val detach_operation: Option[() => Unit] = container match { case floating: FloatingWindowContainer => Untyped.get[AnyRef](Untyped.get[AnyRef](floating, "entry"), "win") match { case dockable: Dockable => dockable.detach_operation case _ => None } case panel: PanelWindowContainer => - val entries = Untyped.get[java.util.List[AnyRef]](panel, "dockables").toArray + val entries = Untyped.get[JList[AnyRef]](panel, "dockables").toArray val wins = (for { entry <- entries.iterator if Untyped.get[String](Untyped.get(entry, "factory"), "name") == dockable_name win = Untyped.get[Any](entry, "win") if win != null } yield win).toList wins match { case List(dockable: Dockable) => dockable.detach_operation case _ => None } case _ => None } if (detach_operation.isDefined) { val detach_item = new JMenuItem("Detach") detach_item.addActionListener(new ActionListener { def actionPerformed(evt: ActionEvent): Unit = detach_operation.get.apply() }) menu.add(detach_item) } menu } } } diff --git a/src/Tools/jEdit/src/fold_handling.scala b/src/Tools/jEdit/src/fold_handling.scala --- a/src/Tools/jEdit/src/fold_handling.scala +++ b/src/Tools/jEdit/src/fold_handling.scala @@ -1,79 +1,81 @@ /* Title: Tools/jEdit/src/fold_handling.scala Author: Makarius Handling of folds within the text structure. */ package isabelle.jedit import isabelle._ +import java.util.{List => JList} + import javax.swing.text.Segment import scala.jdk.CollectionConverters._ import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler} object Fold_Handling { /* input: dynamic line context */ class Fold_Handler extends FoldHandler("isabelle") { override def equals(other: Any): Boolean = other match { case that: Fold_Handler => true case _ => false } override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int = Token_Markup.Line_Context.after(buffer, line).structure.depth max 0 override def getPrecedingFoldLevels( - buffer: JEditBuffer, line: Int, seg: Segment, level: Int): java.util.List[Integer] = + buffer: JEditBuffer, line: Int, seg: Segment, level: Int): JList[Integer] = { val structure = Token_Markup.Line_Context.after(buffer, line).structure val result = if (line > 0 && structure.command) Range.inclusive(line - 1, 0, -1).iterator. map(i => Token_Markup.Line_Context.after(buffer, i).structure). takeWhile(_.improper).map(_ => structure.depth max 0).toList else Nil if (result.isEmpty) null else result.map(Integer.valueOf).asJava } } /* output: static document rendering */ class Document_Fold_Handler(private val rendering: JEdit_Rendering) extends FoldHandler("isabelle-document") { override def equals(other: Any): Boolean = other match { case that: Document_Fold_Handler => this.rendering == that.rendering case _ => false } override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int = { def depth(i: Text.Offset): Int = if (i < 0) 0 else { rendering.fold_depth(Text.Range(i, i + 1)) match { case Text.Info(_, d) :: _ => d case _ => 0 } } if (line <= 0) 0 else { val range = JEdit_Lib.line_range(buffer, line - 1) buffer.getFoldLevel(line - 1) - depth(range.start - 1) + depth(range.stop - 1) } } } } diff --git a/src/Tools/jEdit/src/keymap_merge.scala b/src/Tools/jEdit/src/keymap_merge.scala --- a/src/Tools/jEdit/src/keymap_merge.scala +++ b/src/Tools/jEdit/src/keymap_merge.scala @@ -1,259 +1,260 @@ /* Title: Tools/jEdit/src/keymap_merge.scala Author: Makarius Merge of Isabelle shortcuts vs. jEdit keymap. */ package isabelle.jedit import isabelle._ +import java.util.{Properties => JProperties} import java.awt.{Color, Dimension, BorderLayout} import javax.swing.{JPanel, JTable, JScrollPane, JOptionPane} import javax.swing.table.AbstractTableModel import scala.jdk.CollectionConverters._ import org.gjt.sp.jedit.{jEdit, View} import org.gjt.sp.util.GenericGUIUtilities import org.jedit.keymap.{KeymapManager, Keymap} object Keymap_Merge { /** shortcuts **/ private def is_shortcut(property: String): Boolean = (property.endsWith(".shortcut") || property.endsWith(".shortcut2")) && !property.startsWith("options.shortcuts.") class Shortcut(val property: String, val binding: String) { override def toString: String = Properties.Eq(property, binding) def primary: Boolean = property.endsWith(".shortcut") val action: String = Library.try_unsuffix(".shortcut", property) orElse Library.try_unsuffix(".shortcut2", property) getOrElse error("Bad shortcut property: " + quote(property)) val label: String = GenericGUIUtilities.prettifyMenuLabel(jEdit.getProperty(action + ".label", "")) /* ignore wrt. keymap */ private def prop_ignore: String = property + ".ignore" def ignored_keymaps(): List[String] = space_explode(',', jEdit.getProperty(prop_ignore, "")) def is_ignored(keymap_name: String): Boolean = ignored_keymaps().contains(keymap_name) def ignore(keymap_name: String): Unit = jEdit.setProperty(prop_ignore, Library.insert(keymap_name)(ignored_keymaps()).sorted.mkString(",")) def set(keymap: Keymap): Unit = keymap.setShortcut(property, binding) def reset(keymap: Keymap): Unit = keymap.setShortcut(property, null) } /* content wrt. keymap */ - def convert_properties(props: java.util.Properties): List[Shortcut] = + def convert_properties(props: JProperties): List[Shortcut] = if (props == null) Nil else { var result = List.empty[Shortcut] for (entry <- props.asScala) { entry match { case (a: String, b: String) if is_shortcut(a) => result ::= new Shortcut(a, b) case _ => } } result.sortBy(_.property) } def get_shortcut_conflicts(keymap_name: String, keymap: Keymap): List[(Shortcut, List[Shortcut])] = { val keymap_shortcuts = if (keymap == null) Nil - else convert_properties(Untyped.get[java.util.Properties](keymap, "props")) + else convert_properties(Untyped.get[JProperties](keymap, "props")) for (s <- convert_properties(jEdit.getProperties) if !s.is_ignored(keymap_name)) yield { val conflicts = keymap_shortcuts.filter(s1 => s.property == s1.property && s.binding != s1.binding || s.property != s1.property && s.binding == s1.binding && s1.binding != "") (s, conflicts) } } /** table **/ private def conflict_color: Color = PIDE.options.color_value("error_color") private sealed case class Table_Entry(shortcut: Shortcut, head: Option[Int], tail: List[Int]) { override def toString: String = if (head.isEmpty) "" + HTML.output(shortcut.toString) + "" else "" + HTML.output("--- " + shortcut.toString) + "" } private class Table_Model(entries: List[Table_Entry]) extends AbstractTableModel { private val entries_count = entries.length private def has_entry(row: Int): Boolean = 0 <= row && row <= entries_count private def get_entry(row: Int): Option[Table_Entry] = if (has_entry(row)) Some(entries(row)) else None private val selected = Synchronized[Set[Int]]( (for ((e, i) <- entries.iterator.zipWithIndex if e.head.isEmpty) yield i).toSet) private def is_selected(row: Int): Boolean = selected.value.contains(row) private def select(head: Int, tail: List[Int], b: Boolean): Unit = selected.change(set => if (b) set + head -- tail else set - head ++ tail) def apply(keymap_name: String, keymap: Keymap): Unit = { GUI_Thread.require {} for ((entry, row) <- entries.iterator.zipWithIndex if entry.head.isEmpty) { val b = is_selected(row) if (b) { entry.tail.foreach(i => entries(i).shortcut.reset(keymap)) entry.shortcut.set(keymap) } else entry.shortcut.ignore(keymap_name) } } override def getColumnCount: Int = 2 override def getColumnClass(i: Int): Class[_ <: Object] = if (i == 0) classOf[java.lang.Boolean] else classOf[Object] override def getColumnName(i: Int): String = if (i == 0) " " else if (i == 1) "Keyboard shortcut" else "???" override def getRowCount: Int = entries_count override def getValueAt(row: Int, column: Int): AnyRef = { get_entry(row) match { case Some(entry) if column == 0 => java.lang.Boolean.valueOf(is_selected(row)) case Some(entry) if column == 1 => entry case _ => null } } override def isCellEditable(row: Int, column: Int): Boolean = has_entry(row) && column == 0 override def setValueAt(value: AnyRef, row: Int, column: Int): Unit = { value match { case obj: java.lang.Boolean if has_entry(row) && column == 0 => val b = obj.booleanValue val entry = entries(row) entry.head match { case None => select(row, entry.tail, b) case Some(head_row) => val head_entry = entries(head_row) select(head_row, head_entry.tail, !b) } GUI_Thread.later { fireTableDataChanged() } case _ => } } } private class Table(table_model: Table_Model) extends JPanel(new BorderLayout) { private val cell_size = GenericGUIUtilities.defaultTableCellSize() private val table_size = new Dimension(cell_size.width * 2, cell_size.height * 15) val table = new JTable(table_model) table.setShowGrid(false) table.setIntercellSpacing(new Dimension(0, 0)) table.setRowHeight(cell_size.height + 2) table.setPreferredScrollableViewportSize(table_size) table.setFillsViewportHeight(true) table.getTableHeader.setReorderingAllowed(false) table.getColumnModel.getColumn(0).setPreferredWidth(30) table.getColumnModel.getColumn(0).setMinWidth(30) table.getColumnModel.getColumn(0).setMaxWidth(30) table.getColumnModel.getColumn(0).setResizable(false) table.getColumnModel.getColumn(1).setPreferredWidth(table_size.width - 30) val scroller = new JScrollPane(table) scroller.getViewport.setBackground(table.getBackground) scroller.setPreferredSize(table_size) add(scroller, BorderLayout.CENTER) } /** check with optional dialog **/ def check_dialog(view: View): Unit = { GUI_Thread.require {} val keymap_manager = jEdit.getKeymapManager val keymap_name = jEdit.getProperty("keymap.current", KeymapManager.DEFAULT_KEYMAP_NAME) val keymap = keymap_manager.getKeymap(keymap_name) match { case null => keymap_manager.getKeymap(KeymapManager.DEFAULT_KEYMAP_NAME) case keymap => keymap } val all_shortcut_conflicts = get_shortcut_conflicts(keymap_name, keymap) val no_shortcut_conflicts = for ((s, cs) <- all_shortcut_conflicts if cs.isEmpty) yield s val shortcut_conflicts = all_shortcut_conflicts.filter(_._2.nonEmpty) val table_entries = for { ((shortcut, conflicts), i) <- shortcut_conflicts zip shortcut_conflicts.scanLeft(0)({ case (i, (_, cs)) => i + 1 + cs.length }) entry <- Table_Entry(shortcut, None, ((i + 1) to (i + conflicts.length)).toList) :: conflicts.map(Table_Entry(_, Some(i), Nil)) } yield entry val table_model = new Table_Model(table_entries) if (table_entries.nonEmpty && GUI.confirm_dialog(view, "Pending Isabelle/jEdit keymap changes", JOptionPane.OK_CANCEL_OPTION, "The following Isabelle keymap changes are in conflict with the current", "jEdit keymap " + quote(keymap_name) + ":", new Table(table_model), "Selected shortcuts will be applied, unselected changes will be ignored.", "Results are stored in $JEDIT_SETTINGS/properties and $JEDIT_SETTINGS/keymaps/.") == 0) { table_model.apply(keymap_name, keymap) } no_shortcut_conflicts.foreach(_.set(keymap)) keymap.save() jEdit.saveSettings() jEdit.propertiesChanged() } } diff --git a/src/Tools/jEdit/src/syntax_style.scala b/src/Tools/jEdit/src/syntax_style.scala --- a/src/Tools/jEdit/src/syntax_style.scala +++ b/src/Tools/jEdit/src/syntax_style.scala @@ -1,189 +1,189 @@ /* Title: Tools/jEdit/src/syntax_style.scala Author: Makarius Support for extended syntax styles: subscript, superscript, bold, user fonts. */ package isabelle.jedit import isabelle._ +import java.util.{Map => JMap} import java.awt.{Font, Color} import java.awt.font.TextAttribute import java.awt.geom.AffineTransform import org.gjt.sp.util.SyntaxUtilities import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle} import org.gjt.sp.jedit.textarea.TextArea object Syntax_Style { /* extended syntax styles */ private val plain_range: Int = JEditToken.ID_COUNT private def check_range(i: Int): Unit = require(0 <= i && i < plain_range, "bad syntax style range") def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte } def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte } def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte } def user_font(idx: Int, i: Byte): Byte = { check_range(i); (i + (4 + idx) * plain_range).toByte } val hidden: Byte = (6 * plain_range).toByte val control: Byte = (hidden + JEditToken.DIGIT).toByte private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle = new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, f(style.getFont)) private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle = { font_style(style, font0 => { - val font1 = - font0.deriveFont(java.util.Map.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i))) + val font1 = font0.deriveFont(JMap.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i))) def shift(y: Float): Font = GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble)) val m0 = GUI.line_metrics(font0) val m1 = GUI.line_metrics(font1) val a = m1.getAscent - m0.getAscent val b = (m1.getDescent + m1.getLeading) - (m0.getDescent + m0.getLeading) if (a > 0.0f) shift(a) else if (b > 0.0f) shift(- b) else font1 }) } private def bold_style(style: SyntaxStyle): SyntaxStyle = font_style(style, font => font.deriveFont(if (font.isBold) Font.PLAIN else Font.BOLD)) val hidden_color: Color = new Color(255, 255, 255, 0) object Extender extends SyntaxUtilities.StyleExtender { val max_user_fonts = 2 if (Symbol.font_names.length > max_user_fonts) error("Too many user symbol fonts (" + max_user_fonts + " permitted): " + Symbol.font_names.mkString(", ")) override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = { val style0 = styles(0) val font0 = style0.getFont val new_styles = Array.fill[SyntaxStyle](java.lang.Byte.MAX_VALUE)(styles(0)) for (i <- 0 until plain_range) { val style = styles(i) new_styles(i) = style new_styles(subscript(i.toByte)) = script_style(style, -1) new_styles(superscript(i.toByte)) = script_style(style, 1) new_styles(bold(i.toByte)) = bold_style(style) for (idx <- 0 until max_user_fonts) new_styles(user_font(idx, i.toByte)) = style for ((family, idx) <- Symbol.font_index) new_styles(user_font(idx, i.toByte)) = font_style(style, GUI.imitate_font(_, family)) } new_styles(hidden) = new SyntaxStyle(hidden_color, null, GUI.transform_font(new Font(font0.getFamily, 0, 1), AffineTransform.getScaleInstance(2.0, font0.getSize.toDouble))) new_styles(control) = new SyntaxStyle(style0.getForegroundColor, style0.getBackgroundColor, { val font_style = (if (font0.isItalic) 0 else Font.ITALIC) | (if (font0.isBold) 0 else Font.BOLD) new Font(font0.getFamily, font_style, font0.getSize) }) new_styles } } private def control_style(sym: String): Option[Byte => Byte] = if (sym == Symbol.sub_decoded) Some(subscript) else if (sym == Symbol.sup_decoded) Some(superscript) else if (sym == Symbol.bold_decoded) Some(bold) else None def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] = { var result = Map[Text.Offset, Byte => Byte]() def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte): Unit = { for (i <- start until stop) result += (i -> style) } var offset = 0 var control_sym = "" for (sym <- Symbol.iterator(text)) { val end_offset = offset + sym.length if (control_style(sym).isDefined) control_sym = sym else if (control_sym != "") { if (Symbol.is_controllable(sym) && !Symbol.fonts.isDefinedAt(sym)) { mark(offset - control_sym.length, offset, _ => hidden) mark(offset, end_offset, control_style(control_sym).get) } control_sym = "" } if (Symbol.is_control_encoded(sym)) { val a = offset + Symbol.control_prefix.length val b = end_offset - Symbol.control_suffix.length mark(offset, a, _ => hidden) mark(a, b, _ => control) mark(b, end_offset, _ => hidden) } Symbol.lookup_font(sym) match { case Some(idx) => mark(offset, end_offset, user_font(idx, _)) case _ => } offset = end_offset } result } /* editing support for control symbols */ def edit_control_style(text_area: TextArea, control_sym: String): Unit = { GUI_Thread.assert {} val buffer = text_area.getBuffer val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control_sym) def update_style(text: String): String = { val result = new StringBuilder for (sym <- Symbol.iterator(text) if !HTML.is_control(sym)) { if (Symbol.is_controllable(sym)) result ++= control_decoded result ++= sym } result.toString } text_area.getSelection.foreach(sel => { val before = JEdit_Lib.point_range(buffer, sel.getStart - 1) JEdit_Lib.get_text(buffer, before) match { case Some(s) if HTML.is_control(s) => text_area.extendSelection(before.start, before.stop) case _ => } }) text_area.getSelection.toList match { case Nil => text_area.setSelectedText(control_decoded) case sels => JEdit_Lib.buffer_edit(buffer) { sels.foreach(sel => text_area.setSelectedText(sel, update_style(text_area.getSelectedText(sel)))) } } } } diff --git a/src/Tools/jEdit/src/text_structure.scala b/src/Tools/jEdit/src/text_structure.scala --- a/src/Tools/jEdit/src/text_structure.scala +++ b/src/Tools/jEdit/src/text_structure.scala @@ -1,355 +1,357 @@ /* Title: Tools/jEdit/src/text_structure.scala Author: Makarius Text structure based on Isabelle/Isar outer syntax. */ package isabelle.jedit import isabelle._ +import java.util.{List => JList} + import org.gjt.sp.jedit.indent.{IndentRule, IndentAction} import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection} import org.gjt.sp.jedit.buffer.JEditBuffer import org.gjt.sp.jedit.Buffer object Text_Structure { /* token navigator */ class Navigator(syntax: Outer_Syntax, buffer: JEditBuffer, comments: Boolean) { val limit: Int = PIDE.options.value.int("jedit_structure_limit") max 0 def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = { val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim) if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper) } def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = { val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim) if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper) } } /* indentation */ object Indent_Rule extends IndentRule { private val keyword_open = Keyword.theory_goal ++ Keyword.proof_open private val keyword_close = Keyword.proof_close def apply(buffer: JEditBuffer, current_line: Int, prev_line0: Int, prev_prev_line0: Int, - actions: java.util.List[IndentAction]): Unit = + actions: JList[IndentAction]): Unit = { Isabelle.buffer_syntax(buffer) match { case Some(syntax) => val keywords = syntax.keywords val nav = new Navigator(syntax, buffer, true) val indent_size = buffer.getIndentSize def line_indent(line: Int): Int = if (line < 0 || line >= buffer.getLineCount) 0 else buffer.getCurrentIndentForLine(line, null) def line_head(line: Int): Option[Text.Info[Token]] = nav.iterator(line, 1).nextOption() def head_is_quasi_command(line: Int): Boolean = line_head(line) match { case None => false case Some(Text.Info(_, tok)) => keywords.is_quasi_command(tok) } val prev_line: Int = Range.inclusive(current_line - 1, 0, -1).find(line => Token_Markup.Line_Context.before(buffer, line).get_context == Scan.Finished && (!Token_Markup.Line_Context.after(buffer, line).structure.improper || Token_Markup.Line_Context.after(buffer, line).structure.blank)) getOrElse -1 def prev_line_command: Option[Token] = nav.reverse_iterator(prev_line, 1). collectFirst({ case Text.Info(_, tok) if tok.is_begin_or_command => tok }) def prev_line_span: Iterator[Token] = nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_begin_or_command) def prev_span: Iterator[Token] = nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_begin_or_command) val script_indent: Text.Info[Token] => Int = { val opt_rendering: Option[JEdit_Rendering] = if (PIDE.options.value.bool("jedit_indent_script")) GUI_Thread.now { (for { text_area <- JEdit_Lib.jedit_text_areas(buffer) doc_view <- Document_View.get(text_area) } yield doc_view.get_rendering()).nextOption() } else None val limit = PIDE.options.value.int("jedit_indent_script_limit") (info: Text.Info[Token]) => opt_rendering match { case Some(rendering) if keywords.is_command(info.info, Keyword.prf_script) => (rendering.indentation(info.range) min limit) max 0 case _ => 0 } } def indent_indent(tok: Token): Int = if (keywords.is_command(tok, keyword_open)) indent_size else if (keywords.is_command(tok, keyword_close)) - indent_size else 0 def indent_offset(tok: Token): Int = if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size else 0 def indent_structure: Int = nav.reverse_iterator(current_line - 1).scanLeft((0, false))( { case ((ind, _), Text.Info(range, tok)) => val ind1 = ind + indent_indent(tok) if (tok.is_begin_or_command && !keywords.is_command(tok, Keyword.prf_script)) { val line = buffer.getLineOfOffset(range.start) line_head(line) match { case Some(info) if info.info == tok => (ind1 + indent_offset(tok) + line_indent(line), true) case _ => (ind1, false) } } else (ind1, false) }).collectFirst({ case (i, true) => i }).getOrElse(0) def indent_brackets: Int = prev_line_span.foldLeft(0) { case (i, tok) => if (tok.is_open_bracket) i + indent_size else if (tok.is_close_bracket) i - indent_size else i } def indent_extra: Int = if (prev_span.exists(keywords.is_quasi_command)) indent_size else 0 val indent = if (Token_Markup.Line_Context.before(buffer, current_line).get_context != Scan.Finished) line_indent(current_line) else if (Token_Markup.Line_Context.after(buffer, current_line).structure.blank) 0 else { line_head(current_line) match { case Some(info) => val tok = info.info if (tok.is_begin || keywords.is_before_command(tok) || keywords.is_command(tok, Keyword.theory)) 0 else if (keywords.is_command(tok, Keyword.proof_enclose)) indent_structure + script_indent(info) - indent_offset(tok) else if (keywords.is_command(tok, Keyword.proof)) (indent_structure + script_indent(info) - indent_offset(tok)) max indent_size else if (tok.is_command) indent_structure - indent_offset(tok) else { prev_line_command match { case None => val extra = (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match { case (true, true) | (false, false) => 0 case (true, false) => - indent_extra case (false, true) => indent_extra } line_indent(prev_line) + indent_brackets + extra - indent_offset(tok) case Some(prev_tok) => indent_structure + indent_brackets + indent_size - indent_offset(tok) - indent_offset(prev_tok) - indent_indent(prev_tok) } } case None => prev_line_command match { case None => val extra = if (head_is_quasi_command(prev_line)) indent_extra else 0 line_indent(prev_line) + indent_brackets + extra case Some(prev_tok) => indent_structure + indent_brackets + indent_size - indent_offset(prev_tok) - indent_indent(prev_tok) } } } actions.clear() actions.add(new IndentAction.AlignOffset(indent max 0)) case None => } } } def line_content(buffer: JEditBuffer, keywords: Keyword.Keywords, range: Text.Range, ctxt: Scan.Line_Context): (List[Token], Scan.Line_Context) = { val text = JEdit_Lib.get_text(buffer, range).getOrElse("") val (toks, ctxt1) = Token.explode_line(keywords, text, ctxt) val toks1 = toks.filterNot(_.is_space) (toks1, ctxt1) } def split_line_content(buffer: JEditBuffer, keywords: Keyword.Keywords, line: Int, caret: Int) : (List[Token], List[Token]) = { val line_range = JEdit_Lib.line_range(buffer, line) val ctxt0 = Token_Markup.Line_Context.before(buffer, line).get_context val (toks1, ctxt1) = line_content(buffer, keywords, Text.Range(line_range.start, caret), ctxt0) val (toks2, _) = line_content(buffer, keywords, Text.Range(caret, line_range.stop), ctxt1) (toks1, toks2) } /* structure matching */ object Matcher extends StructureMatcher { private def find_block( open: Token => Boolean, close: Token => Boolean, reset: Token => Boolean, restrict: Token => Boolean, it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] = { val range1 = it.next().range it.takeWhile(info => !info.info.is_command || restrict(info.info)). scanLeft((range1, 1))( { case ((r, d), Text.Info(range, tok)) => if (open(tok)) (range, d + 1) else if (close(tok)) (range, d - 1) else if (reset(tok)) (range, 0) else (r, d) } ).collectFirst({ case (range2, 0) => (range1, range2) }) } private def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] = { val buffer = text_area.getBuffer val caret_line = text_area.getCaretLine val caret = text_area.getCaretPosition Isabelle.buffer_syntax(text_area.getBuffer) match { case Some(syntax) => val keywords = syntax.keywords val nav = new Navigator(syntax, buffer, false) def caret_iterator(): Iterator[Text.Info[Token]] = nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret)) def reverse_caret_iterator(): Iterator[Text.Info[Token]] = nav.reverse_iterator(caret_line).dropWhile(info => !info.range.touches(caret)) nav.iterator(caret_line, 1).find(info => info.range.touches(caret)) match { case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.theory_goal) => find_block( keywords.is_command(_, Keyword.proof_goal), keywords.is_command(_, Keyword.qed), keywords.is_command(_, Keyword.qed_global), t => keywords.is_command(t, Keyword.diag) || keywords.is_command(t, Keyword.proof), caret_iterator()) case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.proof_goal) => find_block( keywords.is_command(_, Keyword.proof_goal), keywords.is_command(_, Keyword.qed), _ => false, t => keywords.is_command(t, Keyword.diag) || keywords.is_command(t, Keyword.proof), caret_iterator()) case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed_global) => reverse_caret_iterator().find(info => keywords.is_command(info.info, Keyword.theory)) match { case Some(Text.Info(range2, tok)) if keywords.is_command(tok, Keyword.theory_goal) => Some((range1, range2)) case _ => None } case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed) => find_block( keywords.is_command(_, Keyword.qed), t => keywords.is_command(t, Keyword.proof_goal) || keywords.is_command(t, Keyword.theory_goal), _ => false, t => keywords.is_command(t, Keyword.diag) || keywords.is_command(t, Keyword.proof) || keywords.is_command(t, Keyword.theory_goal), reverse_caret_iterator()) case Some(Text.Info(range1, tok)) if tok.is_begin => find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator()) case Some(Text.Info(range1, tok)) if tok.is_end => find_block(_.is_end, _.is_begin, _ => false, _ => true, reverse_caret_iterator()) match { case Some((_, range2)) => reverse_caret_iterator(). dropWhile(info => info.range != range2). dropWhile(info => info.range == range2). find(info => info.info.is_command || info.info.is_begin) match { case Some(Text.Info(range3, tok)) => if (keywords.is_command(tok, Keyword.theory_block)) Some((range1, range3)) else Some((range1, range2)) case None => None } case None => None } case _ => None } case None => None } } def getMatch(text_area: TextArea): StructureMatcher.Match = find_pair(text_area) match { case Some((_, range)) => val line = text_area.getBuffer.getLineOfOffset(range.start) new StructureMatcher.Match(Matcher, line, range.start, line, range.stop) case None => null } def selectMatch(text_area: TextArea): Unit = { def get_span(offset: Text.Offset): Option[Text.Range] = for { syntax <- Isabelle.buffer_syntax(text_area.getBuffer) span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset) } yield span.range find_pair(text_area) match { case Some((r1, r2)) => (get_span(r1.start), get_span(r2.start)) match { case (Some(range1), Some(range2)) => val start = range1.start min range2.start val stop = range1.stop max range2.stop text_area.moveCaretPosition(stop, false) if (!text_area.isMultipleSelectionEnabled) text_area.selectNone text_area.addToSelection(new Selection.Range(start, stop)) case _ => } case None => } } } } diff --git a/src/Tools/jEdit/src/token_markup.scala b/src/Tools/jEdit/src/token_markup.scala --- a/src/Tools/jEdit/src/token_markup.scala +++ b/src/Tools/jEdit/src/token_markup.scala @@ -1,321 +1,322 @@ /* Title: Tools/jEdit/src/token_markup.scala Author: Makarius Outer syntax token markup. */ package isabelle.jedit import isabelle._ +import java.util.{List => JList} + import javax.swing.text.Segment import org.gjt.sp.jedit.{Mode, Buffer} import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler, ParserRuleSet, ModeProvider, XModeHandler} import org.gjt.sp.jedit.indent.IndentRule import org.gjt.sp.jedit.buffer.JEditBuffer object Token_Markup { /* line context */ def mode_rule_set(mode: String): ParserRuleSet = new ParserRuleSet(mode, "MAIN") object Line_Context { def init(mode: String): Line_Context = new Line_Context(mode, Some(Scan.Finished), Line_Structure.init) def refresh(buffer: JEditBuffer, line: Int): Unit = buffer.markTokens(line, DummyTokenHandler.INSTANCE) def before(buffer: JEditBuffer, line: Int): Line_Context = if (line == 0) init(JEdit_Lib.buffer_mode(buffer)) else after(buffer, line - 1) def after(buffer: JEditBuffer, line: Int): Line_Context = { val line_mgr = JEdit_Lib.buffer_line_manager(buffer) def context = line_mgr.getLineContext(line) match { case c: Line_Context => Some(c) case _ => None } context getOrElse { refresh(buffer, line) context getOrElse init(JEdit_Lib.buffer_mode(buffer)) } } } class Line_Context( val mode: String, val context: Option[Scan.Line_Context], val structure: Line_Structure) extends TokenMarker.LineContext(mode_rule_set(mode), null) { def get_context: Scan.Line_Context = context.getOrElse(Scan.Finished) override def hashCode: Int = (mode, context, structure).hashCode override def equals(that: Any): Boolean = that match { case other: Line_Context => mode == other.mode && context == other.context && structure == other.structure case _ => false } } /* tokens from line (inclusive) */ private def try_line_tokens(syntax: Outer_Syntax, buffer: JEditBuffer, line: Int) : Option[List[Token]] = { val line_context = Line_Context.before(buffer, line) for { ctxt <- line_context.context text <- JEdit_Lib.get_text(buffer, JEdit_Lib.line_range(buffer, line)) } yield Token.explode_line(syntax.keywords, text, ctxt)._1 } def line_token_iterator( syntax: Outer_Syntax, buffer: JEditBuffer, start_line: Int, end_line: Int): Iterator[Text.Info[Token]] = for { line <- Range(start_line max 0, end_line min buffer.getLineCount).iterator tokens <- try_line_tokens(syntax, buffer, line).iterator starts = tokens.iterator.scanLeft(buffer.getLineStartOffset(line))( (i, tok) => i + tok.source.length) (i, tok) <- starts zip tokens.iterator } yield Text.Info(Text.Range(i, i + tok.source.length), tok) def line_token_reverse_iterator( syntax: Outer_Syntax, buffer: JEditBuffer, start_line: Int, end_line: Int): Iterator[Text.Info[Token]] = for { line <- Range(start_line min (buffer.getLineCount - 1), end_line max -1, -1).iterator tokens <- try_line_tokens(syntax, buffer, line).iterator stops = tokens.reverseIterator.scanLeft(buffer.getLineEndOffset(line) min buffer.getLength)( (i, tok) => i - tok.source.length) (i, tok) <- stops zip tokens.reverseIterator } yield Text.Info(Text.Range(i - tok.source.length, i), tok) /* tokens from offset (inclusive) */ def token_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset): Iterator[Text.Info[Token]] = if (JEdit_Lib.buffer_range(buffer).contains(offset)) line_token_iterator(syntax, buffer, buffer.getLineOfOffset(offset), buffer.getLineCount). dropWhile(info => !info.range.contains(offset)) else Iterator.empty def token_reverse_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset): Iterator[Text.Info[Token]] = if (JEdit_Lib.buffer_range(buffer).contains(offset)) line_token_reverse_iterator(syntax, buffer, buffer.getLineOfOffset(offset), -1). dropWhile(info => !info.range.contains(offset)) else Iterator.empty /* command spans */ def command_span(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset) : Option[Text.Info[Command_Span.Span]] = { val keywords = syntax.keywords def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] = token_reverse_iterator(syntax, buffer, i). find(info => keywords.is_before_command(info.info) || info.info.is_command) def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] = token_iterator(syntax, buffer, i). find(info => keywords.is_before_command(info.info) || info.info.is_command) if (JEdit_Lib.buffer_range(buffer).contains(offset)) { val start_info = { val info1 = maybe_command_start(offset) info1 match { case Some(Text.Info(range1, tok1)) if tok1.is_command => val info2 = maybe_command_start(range1.start - 1) info2 match { case Some(Text.Info(_, tok2)) if keywords.is_before_command(tok2) => info2 case _ => info1 } case _ => info1 } } val (start_before_command, start, start_next) = start_info match { case Some(Text.Info(range, tok)) => (keywords.is_before_command(tok), range.start, range.stop) case None => (false, 0, 0) } val stop_info = { val info1 = maybe_command_stop(start_next) info1 match { case Some(Text.Info(range1, tok1)) if tok1.is_command && start_before_command => maybe_command_stop(range1.stop) case _ => info1 } } val stop = stop_info match { case Some(Text.Info(range, _)) => range.start case None => buffer.getLength } val text = JEdit_Lib.get_text(buffer, Text.Range(start, stop)).getOrElse("") val spans = syntax.parse_spans(text) (spans.iterator.scanLeft(start)(_ + _.length) zip spans.iterator). map({ case (i, span) => Text.Info(Text.Range(i, i + span.length), span) }). find(_.range.contains(offset)) } else None } private def _command_span_iterator( syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset, next_offset: Text.Range => Text.Offset): Iterator[Text.Info[Command_Span.Span]] = new Iterator[Text.Info[Command_Span.Span]] { private var next_span = command_span(syntax, buffer, offset) def hasNext: Boolean = next_span.isDefined def next(): Text.Info[Command_Span.Span] = { val span = next_span.getOrElse(Iterator.empty.next()) next_span = command_span(syntax, buffer, next_offset(span.range)) span } } def command_span_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset) : Iterator[Text.Info[Command_Span.Span]] = _command_span_iterator(syntax, buffer, offset max 0, range => range.stop) def command_span_reverse_iterator(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset) : Iterator[Text.Info[Command_Span.Span]] = _command_span_iterator(syntax, buffer, (offset min buffer.getLength) - 1, range => range.start - 1) /* token marker */ class Marker( protected val mode: String, protected val opt_buffer: Option[Buffer]) extends TokenMarker { addRuleSet(mode_rule_set(mode)) override def hashCode: Int = (mode, opt_buffer).hashCode override def equals(that: Any): Boolean = that match { case other: Marker => mode == other.mode && opt_buffer == other.opt_buffer case _ => false } override def toString: String = opt_buffer match { case None => "Marker(" + mode + ")" case Some(buffer) => "Marker(" + mode + "," + JEdit_Lib.buffer_name(buffer) + ")" } override def markTokens(context: TokenMarker.LineContext, handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext = { val line = if (raw_line == null) new Segment else raw_line val line_context = context match { case c: Line_Context => c case _ => Line_Context.init(mode) } val structure = line_context.structure val context1 = { val opt_syntax = opt_buffer match { case Some(buffer) => Isabelle.buffer_syntax(buffer) case None => Isabelle.mode_syntax(mode) } val (styled_tokens, context1) = (line_context.context, opt_syntax) match { case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" => val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt) val styled_tokens = tokens.map(tok => (JEdit_Rendering.ml_token_markup(tok), tok.source)) (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure)) case (Some(ctxt), Some(syntax)) if syntax.has_tokens => val (tokens, ctxt1) = Token.explode_line(syntax.keywords, line, ctxt) val structure1 = structure.update(syntax.keywords, tokens) val styled_tokens = tokens.map(tok => (JEdit_Rendering.token_markup(syntax, tok), tok.source)) (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure1)) case _ => val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString) (List(styled_token), new Line_Context(line_context.mode, None, structure)) } val extended = Syntax_Style.extended(line) def special(i: Int): Boolean = extended.isDefinedAt(i) || line.charAt(i) == '\t' var offset = 0 for ((style, token) <- styled_tokens) { val length = token.length if ((offset until (offset + length)).exists(special)) { for ((c, i) <- Codepoint.iterator_offset(token)) { val style1 = extended.get(offset + i) match { case None => style case Some(ext) => ext(style) } handler.handleToken(line, style1, offset + i, Character.charCount(c), context1) } } else handler.handleToken(line, style, offset, length, context1) offset += length } handler.handleToken(line, JEditToken.END, line.count, 0, context1) context1 } val context2 = context1.intern handler.setLineContext(context2) context2 } } /* mode provider */ class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider { for (mode <- orig_provider.getModes) addMode(mode) override def loadMode(mode: Mode, xmh: XModeHandler): Unit = { super.loadMode(mode, xmh) Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker) Isabelle.indent_rule(mode.getName).foreach(indent_rule => - Untyped.set[java.util.List[IndentRule]]( - mode, "indentRules", java.util.List.of(indent_rule))) + Untyped.set[JList[IndentRule]](mode, "indentRules", JList.of(indent_rule))) } } }