diff --git a/src/Pure/General/path.scala b/src/Pure/General/path.scala --- a/src/Pure/General/path.scala +++ b/src/Pure/General/path.scala @@ -1,323 +1,327 @@ /* Title: Pure/General/path.scala Author: Makarius Algebra of file-system paths: basic POSIX notation, extended by named roots (e.g. //foo) and variables (e.g. $BAR). */ package isabelle import java.util.{Map => JMap} import java.io.{File => JFile} import java.nio.file.{Path => JPath} +import java.net.{URI, URL} import scala.util.matching.Regex object Path { /* path elements */ sealed abstract class Elem private case class Root(name: String) extends Elem private case class Basic(name: String) extends Elem private case class Variable(name: String) extends Elem private case object Parent extends Elem private def err_elem(msg: String, s: String): Nothing = error(msg + " path element " + quote(s)) private val illegal_elem = Set("", "~", "~~", ".", "..") private val illegal_char = "/\\$:\"'<>|?*" private def check_elem(s: String): String = if (illegal_elem.contains(s)) err_elem("Illegal", s) else { for (c <- s) { if (c.toInt < 32) err_elem("Illegal control character " + c.toInt + " in", s) if (illegal_char.contains(c)) err_elem("Illegal character " + quote(c.toString) + " in", s) } s } private def root_elem(s: String): Elem = Root(check_elem(s)) private def basic_elem(s: String): Elem = Basic(check_elem(s)) private def variable_elem(s: String): Elem = Variable(check_elem(s)) private def apply_elem(y: Elem, xs: List[Elem]): List[Elem] = (y, xs) match { case (Root(_), _) => List(y) case (Parent, Root(_) :: _) => xs case (Parent, Basic(_) :: rest) => rest case _ => y :: xs } private def norm_elems(elems: List[Elem]): List[Elem] = elems.foldRight(List.empty[Elem])(apply_elem) private def implode_elem(elem: Elem, short: Boolean): String = elem match { case Root("") => "" case Root(s) => "//" + s case Basic(s) => s case Variable("USER_HOME") if short => "~" case Variable("ISABELLE_HOME") if short => "~~" case Variable(s) => "$" + s case Parent => ".." } private def squash_elem(elem: Elem): String = elem match { case Root("") => "ROOT" case Root(s) => "SERVER_" + s case Basic(s) => s case Variable(s) => s case Parent => "PARENT" } /* path constructors */ val current: Path = new Path(Nil) val root: Path = new Path(List(Root(""))) def named_root(s: String): Path = new Path(List(root_elem(s))) def make(elems: List[String]): Path = new Path(elems.reverse.map(basic_elem)) def basic(s: String): Path = new Path(List(basic_elem(s))) def variable(s: String): Path = new Path(List(variable_elem(s))) val parent: Path = new Path(List(Parent)) val USER_HOME: Path = variable("USER_HOME") val ISABELLE_HOME: Path = variable("ISABELLE_HOME") /* explode */ def explode(str: String): Path = { def explode_elem(s: String): Elem = try { if (s == "..") Parent else if (s == "~") Variable("USER_HOME") else if (s == "~~") Variable("ISABELLE_HOME") else if (s.startsWith("$")) variable_elem(s.substring(1)) else basic_elem(s) } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in " + quote(str)) } val ss = space_explode('/', str) val r = ss.takeWhile(_.isEmpty).length val es = ss.dropWhile(_.isEmpty) val (roots, raw_elems) = if (r == 0) (Nil, es) else if (r == 1) (List(Root("")), es) else if (es.isEmpty) (List(Root("")), Nil) else (List(root_elem(es.head)), es.tail) val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem) new Path(norm_elems(elems reverse_::: roots)) } def is_wellformed(str: String): Boolean = try { explode(str); true } catch { case ERROR(_) => false } def is_valid(str: String): Boolean = try { explode(str).expand; true } catch { case ERROR(_) => false } def split(str: String): List[Path] = space_explode(':', str).filterNot(_.isEmpty).map(explode) /* encode */ val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode)) /* reserved names */ private val reserved_windows: Set[String] = Set("CON", "PRN", "AUX", "NUL", "COM1", "COM2", "COM3", "COM4", "COM5", "COM6", "COM7", "COM8", "COM9", "LPT1", "LPT2", "LPT3", "LPT4", "LPT5", "LPT6", "LPT7", "LPT8", "LPT9") def is_reserved(name: String): Boolean = Long_Name.explode(name).exists(a => reserved_windows.contains(Word.uppercase(a))) /* case-insensitive names */ def check_case_insensitive(paths: List[Path]): Unit = { val table = paths.foldLeft(Multi_Map.empty[String, String]) { case (tab, path) => val name = path.expand.implode tab.insert(Word.lowercase(name), name) } val collisions = (for { (_, coll) <- table.iterator_list if coll.length > 1 } yield coll).toList.flatten if (collisions.nonEmpty) { error(("Collision of file names due case-insensitivity:" :: collisions).mkString("\n ")) } } } final class Path private( protected val elems: List[Path.Elem] // reversed elements ) { override def hashCode: Int = elems.hashCode override def equals(that: Any): Boolean = that match { case other: Path => elems == other.elems case _ => false } def is_current: Boolean = elems.isEmpty def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root] def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false } def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false } def all_basic: Boolean = elems.forall(_.isInstanceOf[Path.Basic]) def starts_basic: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Basic] def +(other: Path): Path = new Path(other.elems.foldRight(elems)(Path.apply_elem)) /* implode */ private def gen_implode(short: Boolean): String = elems match { case Nil => "." case List(Path.Root("")) => "/" case _ => elems.map(Path.implode_elem(_, short)).reverse.mkString("/") } def implode: String = gen_implode(false) def implode_short: String = gen_implode(true) override def toString: String = quote(implode) /* base element */ private def split_path: (Path, String) = elems match { case Path.Basic(s) :: xs => (new Path(xs), s) case _ => error("Cannot split path into dir/base: " + toString) } def dir: Path = split_path._1 def base: Path = new Path(List(Path.Basic(split_path._2))) def ends_with(a: String): Boolean = elems match { case Path.Basic(b) :: _ => b.endsWith(a) case _ => false } def is_java: Boolean = ends_with(".java") def is_scala: Boolean = ends_with(".scala") def is_pdf: Boolean = ends_with(".pdf") def ext(e: String): Path = if (e == "") this else { val (prfx, s) = split_path prfx + Path.basic(s + "." + e) } def xz: Path = ext("xz") def xml: Path = ext("xml") def html: Path = ext("html") def tex: Path = ext("tex") def pdf: Path = ext("pdf") def thy: Path = ext("thy") def tar: Path = ext("tar") def gz: Path = ext("gz") def log: Path = ext("log") def orig: Path = ext("orig") def patch: Path = ext("patch") def shasum: Path = ext("shasum") def backup: Path = { val (prfx, s) = split_path prfx + Path.basic(s + "~") } def backup2: Path = { val (prfx, s) = split_path prfx + Path.basic(s + "~~") } def exe: Path = ext("exe") def platform_exe: Path = if (Platform.is_windows) exe else this private val Ext = new Regex("(.*)\\.([^.]*)") def split_ext: (Path, String) = { val (prefix, base) = split_path base match { case Ext(b, e) => (prefix + Path.basic(b), e) case _ => (prefix + Path.basic(base), "") } } def drop_ext: Path = split_ext._1 def get_ext: String = split_ext._2 def squash: Path = new Path(elems.map(elem => Path.Basic(Path.squash_elem(elem)))) /* expand */ def expand_env(env: JMap[String, String]): Path = { def eval(elem: Path.Elem): List[Path.Elem] = elem match { case Path.Variable(s) => val path = Path.explode(Isabelle_System.getenv_strict(s, env)) if (path.elems.exists(_.isInstanceOf[Path.Variable])) error("Illegal path variable nesting: " + Properties.Eq(s, path.toString)) else path.elems case x => List(x) } new Path(Path.norm_elems(elems.flatMap(eval))) } def expand: Path = expand_env(Isabelle_System.settings()) def file_name: String = expand.base.implode /* implode wrt. given directories */ def implode_symbolic: String = { val directories = Library.space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse val full_name = expand.implode directories.view.flatMap(a => try { val b = Path.explode(a).expand.implode if (full_name == b) Some(a) else { Library.try_unprefix(b + "/", full_name) match { case Some(name) => Some(a + "/" + name) case None => None } } } catch { case ERROR(_) => None }).headOption.getOrElse(implode) } def position: Position.T = Position.File(implode_symbolic) /* platform files */ def file: JFile = File.platform_file(this) def is_file: Boolean = file.isFile def is_dir: Boolean = file.isDirectory + def uri: URI = file.toURI + def url: URL = uri.toURL + def java_path: JPath = file.toPath def absolute_file: JFile = File.absolute(file) def canonical_file: JFile = File.canonical(file) def absolute: Path = File.path(absolute_file) def canonical: Path = File.path(canonical_file) } diff --git a/src/Tools/jEdit/src/jedit_lib.scala b/src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala +++ b/src/Tools/jEdit/src/jedit_lib.scala @@ -1,358 +1,358 @@ /* Title: Tools/jEdit/src/jedit_lib.scala Author: Makarius Misc library functions for jEdit. */ package isabelle.jedit import isabelle._ import java.io.{File => JFile} import java.awt.{Component, Container, GraphicsEnvironment, Point, Rectangle, Dimension, Toolkit} import java.awt.event.{InputEvent, KeyEvent, KeyListener} import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities} import scala.util.parsing.input.CharSequenceReader import scala.jdk.CollectionConverters._ import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane} import org.gjt.sp.jedit.io.{FileVFS, VFSManager} import org.gjt.sp.jedit.gui.{KeyEventWorkaround, KeyEventTranslator} import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager} import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter} object JEdit_Lib { /* jEdit directories */ def directories: List[JFile] = (Option(jEdit.getSettingsDirectory).toList ::: List(jEdit.getJEditHome)).map(new JFile(_)) /* window geometry measurement */ private lazy val dummy_window = new JWindow final case class Window_Geometry(width: Int, height: Int, inner_width: Int, inner_height: Int) { def deco_width: Int = width - inner_width def deco_height: Int = height - inner_height } def window_geometry(outer: Container, inner: Component): Window_Geometry = { GUI_Thread.require {} val old_content = dummy_window.getContentPane dummy_window.setContentPane(outer) dummy_window.pack dummy_window.revalidate() val geometry = Window_Geometry( dummy_window.getWidth, dummy_window.getHeight, inner.getWidth, inner.getHeight) dummy_window.setContentPane(old_content) geometry } /* files */ def is_file(name: String): Boolean = VFSManager.getVFSForPath(name).isInstanceOf[FileVFS] def check_file(name: String): Option[JFile] = if (is_file(name)) Some(new JFile(name)) else None /* buffers */ def buffer_text(buffer: JEditBuffer): String = buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } def buffer_reader(buffer: JEditBuffer): CharSequenceReader = Scan.char_reader(buffer.getSegment(0, buffer.getLength)) def buffer_mode(buffer: JEditBuffer): String = { val mode = buffer.getMode if (mode == null) "" else { val name = mode.getName if (name == null) "" else name } } def buffer_line_manager(buffer: JEditBuffer): LineManager = Untyped.get[LineManager](buffer, "lineMgr") def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath def buffer_file(buffer: Buffer): Option[JFile] = check_file(buffer_name(buffer)) def buffer_undo_in_progress[A](buffer: JEditBuffer, body: => A): A = { val undo_in_progress = buffer.isUndoInProgress def set(b: Boolean): Unit = Untyped.set[Boolean](buffer, "undoInProgress", b) try { set(true); body } finally { set(undo_in_progress) } } /* main jEdit components */ def jedit_buffers(): Iterator[Buffer] = jEdit.getBufferManager().getBuffers().asScala.iterator def jedit_buffer(name: String): Option[Buffer] = jedit_buffers().find(buffer => buffer_name(buffer) == name) def jedit_buffer(name: Document.Node.Name): Option[Buffer] = jedit_buffer(name.node) def jedit_views(): Iterator[View] = jEdit.getViewManager().getViews().asScala.iterator def jedit_view(view: View = null): View = if (view == null) jEdit.getActiveView() else view def jedit_edit_panes(view: View): Iterator[EditPane] = if (view == null) Iterator.empty else view.getEditPanes().iterator.filter(_ != null) def jedit_text_areas(view: View): Iterator[JEditTextArea] = if (view == null) Iterator.empty else view.getEditPanes().iterator.filter(_ != null).map(_.getTextArea).filter(_ != null) def jedit_text_areas(): Iterator[JEditTextArea] = jedit_views().flatMap(jedit_text_areas) def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = jedit_text_areas().filter(_.getBuffer == buffer) def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = { try { buffer.readLock(); body } finally { buffer.readUnlock() } } def buffer_edit[A](buffer: JEditBuffer)(body: => A): A = { try { buffer.beginCompoundEdit(); body } finally { buffer.endCompoundEdit() } } /* get text */ def get_text(buffer: JEditBuffer, range: Text.Range): Option[String] = try { Some(buffer.getText(range.start, range.length)) } catch { case _: ArrayIndexOutOfBoundsException => None } /* point range */ def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range = if (offset < 0) Text.Range.offside else buffer_lock(buffer) { def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0) try { val c = text(offset) if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1))) Text.Range(offset, offset + 2) else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1))) Text.Range(offset - 1, offset + 1) else Text.Range(offset, offset + 1) } catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) } } /* text ranges */ def buffer_range(buffer: JEditBuffer): Text.Range = Text.Range(0, buffer.getLength) def line_range(buffer: JEditBuffer, line: Int): Text.Range = Text.Range(buffer.getLineStartOffset(line), buffer.getLineEndOffset(line) min buffer.getLength) def caret_range(text_area: TextArea): Text.Range = point_range(text_area.getBuffer, text_area.getCaretPosition) def visible_range(text_area: TextArea): Option[Text.Range] = { val buffer = text_area.getBuffer val n = text_area.getVisibleLines if (n > 0) { val start = text_area.getScreenLineStartOffset(0) val raw_end = text_area.getScreenLineEndOffset(n - 1) val end = if (raw_end >= 0) raw_end min buffer.getLength else buffer.getLength Some(Text.Range(start, end)) } else None } def invalidate_range(text_area: TextArea, range: Text.Range): Unit = { val buffer = text_area.getBuffer buffer_range(buffer).try_restrict(range) match { case Some(range1) if !range1.is_singularity => try { text_area.invalidateLineRange( buffer.getLineOfOffset(range1.start), buffer.getLineOfOffset(range1.stop)) } catch { case _: ArrayIndexOutOfBoundsException => } case _ => } } def invalidate(text_area: TextArea): Unit = { val visible_lines = text_area.getVisibleLines if (visible_lines > 0) text_area.invalidateScreenLineRange(0, visible_lines) } /* graphics range */ case class Gfx_Range(x: Int, y: Int, length: Int) // NB: jEdit always normalizes \r\n and \r to \n // NB: last line lacks \n def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = { val metric = pretty_metric(text_area.getPainter) val char_width = (metric.unit * metric.average).round.toInt val buffer = text_area.getBuffer val end = buffer.getLength val stop = range.stop val (p, q, r) = try { val p = text_area.offsetToXY(range.start) val (q, r) = if (get_text(buffer, Text.Range(stop - 1, stop)) == Some("\n")) (text_area.offsetToXY(stop - 1), char_width) else if (stop >= end) (text_area.offsetToXY(end), char_width * (stop - end)) else (text_area.offsetToXY(stop), 0) (p, q, r) } catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) } if (p != null && q != null && p.x < q.x + r && p.y == q.y) Some(Gfx_Range(p.x, p.y, q.x + r - p.x)) else None } /* pixel range */ def pixel_range(text_area: TextArea, x: Int, y: Int): Option[Text.Range] = { // coordinates wrt. inner painter component val painter = text_area.getPainter if (0 <= x && x < painter.getWidth && 0 <= y && y < painter.getHeight) { val offset = text_area.xyToOffset(x, y, false) if (offset >= 0) { val range = point_range(text_area.getBuffer, offset) gfx_range(text_area, range) match { case Some(g) if g.x <= x && x < g.x + g.length => Some(range) case _ => None } } else None } else None } /* pretty text metric */ abstract class Pretty_Metric extends Pretty.Metric { def average: Double } def pretty_metric(painter: TextAreaPainter): Pretty_Metric = new Pretty_Metric { def string_width(s: String): Double = painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth val unit: Double = string_width(Symbol.space) max 1.0 val average: Double = string_width("mix") / (3 * unit) def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit } /* icons */ def load_icon(name: String): Icon = { val name1 = if (name.startsWith("idea-icons/")) { - val file = Path.explode("$ISABELLE_IDEA_ICONS").file.toURI.toASCIIString + val file = Path.explode("$ISABELLE_IDEA_ICONS").uri.toASCIIString "jar:" + file + "!/" + name } else name val icon = GUIUtilities.loadIcon(name1) if (icon.getIconWidth < 0 || icon.getIconHeight < 0) error("Bad icon: " + name) else icon } def load_image_icon(name: String): ImageIcon = load_icon(name) match { case icon: ImageIcon => icon case _ => error("Bad image icon: " + name) } /* key event handling */ def request_focus_view(alt_view: View = null): Unit = { val view = if (alt_view != null) alt_view else jEdit.getActiveView() if (view != null) { val text_area = view.getTextArea if (text_area != null) text_area.requestFocus() } } def propagate_key(view: View, evt: KeyEvent): Unit = { if (view != null && !evt.isConsumed) view.getInputHandler().processKeyEvent(evt, View.ACTION_BAR, false) } def key_listener( key_typed: KeyEvent => Unit = _ => (), key_pressed: KeyEvent => Unit = _ => (), key_released: KeyEvent => Unit = _ => () ): KeyListener = { def process_key_event(evt0: KeyEvent, handle: KeyEvent => Unit): Unit = { val evt = KeyEventWorkaround.processKeyEvent(evt0) if (evt != null) handle(evt) } new KeyListener { def keyTyped(evt: KeyEvent): Unit = process_key_event(evt, key_typed) def keyPressed(evt: KeyEvent): Unit = process_key_event(evt, key_pressed) def keyReleased(evt: KeyEvent): Unit = process_key_event(evt, key_released) } } def special_key(evt: KeyEvent): Boolean = { // cf. 5.2.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java val mod = evt.getModifiersEx (mod & InputEvent.CTRL_DOWN_MASK) != 0 && (mod & InputEvent.ALT_DOWN_MASK) == 0 || (mod & InputEvent.CTRL_DOWN_MASK) == 0 && (mod & InputEvent.ALT_DOWN_MASK) != 0 && !Debug.ALT_KEY_PRESSED_DISABLED || (mod & InputEvent.META_DOWN_MASK) != 0 } def command_modifier(evt: InputEvent): Boolean = (evt.getModifiersEx & Toolkit.getDefaultToolkit.getMenuShortcutKeyMaskEx) != 0 def shift_modifier(evt: InputEvent): Boolean = (evt.getModifiersEx & InputEvent.SHIFT_DOWN_MASK) != 0 def modifier_string(evt: InputEvent): String = KeyEventTranslator.getModifierString(evt) match { case null => "" case s => s } }