--- a/src/Pure/Admin/check_sources.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Pure/Admin/check_sources.scala Fri Dec 30 20:59:38 2022 +0000
@@ -10,7 +10,7 @@
object Check_Sources {
def check_file(path: Path): Unit = {
val file_name = path.implode
- val file_pos = path.position
+ val file_pos = Position.File(path.implode_symbolic)
def line_pos(i: Int) = Position.Line_File(i + 1, file_name)
if (space_explode('/', Word.lowercase(path.expand.drop_ext.implode)).contains("aux"))
--- a/src/Pure/General/path.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Pure/General/path.scala Fri Dec 30 20:59:38 2022 +0000
@@ -312,8 +312,6 @@
} catch { case ERROR(_) => None }).headOption.getOrElse(implode)
}
- def position: Position.T = Position.File(implode_symbolic)
-
/* platform files */
--- a/src/Pure/General/url.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Pure/General/url.scala Fri Dec 30 20:59:38 2022 +0000
@@ -104,11 +104,35 @@
/* generic path notation: local, ssh, rsync, ftp, http */
+ private val separators1 = "/\\"
+ private val separators2 = ":/\\"
+
+ def is_base_name(s: String, suffix: String = ""): Boolean =
+ s.nonEmpty && !s.exists(separators2.contains) && s.endsWith(suffix)
+
+ def get_base_name(s: String, suffix: String = ""): Option[String] = {
+ val i = s.lastIndexWhere(separators2.contains)
+ if (i + 1 >= s.length) None else Library.try_unsuffix(suffix, s.substring(i + 1))
+ }
+
+ def strip_base_name(s: String, suffix: String = ""): Option[String] = {
+ val i = s.lastIndexWhere(separators2.contains)
+ val j = s.lastIndexWhere(c => !separators1.contains(c), end = i)
+ if (i + 1 >= s.length || !s.endsWith(suffix)) None
+ else if (j < 0) Some(s.substring(0, i + 1))
+ else Some(s.substring(0, j + 1))
+ }
+
def append_path(prefix: String, suffix: String): String =
- if (prefix.endsWith(":") || prefix.endsWith("/") || prefix.isEmpty) prefix + suffix
- else if (prefix.endsWith(":.") || prefix.endsWith("/.") || prefix == ".") {
+ if (prefix.endsWith(":") || prefix.endsWith("/") || prefix.endsWith("\\") || prefix.isEmpty) {
+ prefix + suffix
+ }
+ else if (prefix.endsWith(":.") || prefix.endsWith("/.") || prefix.endsWith("\\.") || prefix == ".") {
prefix.substring(0, prefix.length - 1) + suffix
}
+ else if (prefix.contains('\\') || suffix.contains('\\')) {
+ prefix + "\\" + suffix
+ }
else prefix + "/" + suffix
def direct_path(prefix: String): String = append_path(prefix, ".")
--- a/src/Pure/PIDE/command.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Pure/PIDE/command.scala Fri Dec 30 20:59:38 2022 +0000
@@ -450,7 +450,7 @@
for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) }
yield {
val completion =
- if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil
+ if (Url.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil
"Bad theory import " +
Markup.Path(import_name.node).markup(quote(import_name.toString)) +
Position.here(pos) + Completion.report_theories(pos, completion)
--- a/src/Pure/PIDE/document.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Pure/PIDE/document.scala Fri Dec 30 20:59:38 2022 +0000
@@ -114,6 +114,8 @@
case _ => false
}
+ def file_name: String = Url.get_base_name(node).getOrElse("")
+
def path: Path = Path.explode(File.standard_path(node))
def master_dir_path: Path = Path.explode(File.standard_path(master_dir))
--- a/src/Pure/PIDE/line.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Pure/PIDE/line.scala Fri Dec 30 20:59:38 2022 +0000
@@ -34,7 +34,9 @@
sealed case class Position(line: Int = 0, column: Int = 0) {
def line1: Int = line + 1
def column1: Int = column + 1
- def print: String = line1.toString + ":" + column1.toString
+ def print: String =
+ if (column == 0) line1.toString
+ else line1.toString + ":" + column1.toString
def compare(that: Position): Int =
line compare that.line match {
@@ -48,7 +50,7 @@
val lines = logical_lines(text)
val l = line + lines.length - 1
val c = (if (l == line) column else 0) + Library.trim_line(lines.last).length
- Position(l, c)
+ Position(line = l, column = c)
}
}
@@ -61,8 +63,9 @@
}
sealed case class Range(start: Position, stop: Position) {
- if (start.compare(stop) > 0)
+ if (start.compare(stop) > 0) {
error("Bad line range: " + start.print + ".." + stop.print)
+ }
def print: String =
if (start == stop) start.print
@@ -73,7 +76,7 @@
/* positions within document node */
object Node_Position {
- def offside(name: String): Node_Position = Node_Position(name, Position.offside)
+ def offside(name: String): Node_Position = Node_Position(name, pos = Position.offside)
}
sealed case class Node_Position(name: String, pos: Position = Position.zero) {
@@ -134,11 +137,14 @@
def position(text_offset: Text.Offset): Position = {
@tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position = {
lines_rest match {
- case Nil => require(i == 0, "bad Line.position.move"); Position(lines_count)
+ case Nil =>
+ require(i == 0, "bad Line.position.move")
+ Position(line = lines_count)
case line :: ls =>
val n = line.text.length
- if (ls.isEmpty || i <= n)
- Position(lines_count).advance(line.text.substring(n - i))
+ if (ls.isEmpty || i <= n) {
+ Position(line = lines_count).advance(line.text.substring(n - i))
+ }
else move(i - (n + 1), lines_count + 1, ls)
}
}
--- a/src/Pure/PIDE/resources.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Pure/PIDE/resources.scala Fri Dec 30 20:59:38 2022 +0000
@@ -172,7 +172,7 @@
val theory = theory_name(qualifier, Thy_Header.import_name(s))
val literal_import =
literal_theory(theory) && qualifier != sessions_structure.theory_qualifier(theory)
- if (literal_import && !Thy_Header.is_base_name(s)) {
+ if (literal_import && !Url.is_base_name(s)) {
error("Bad import of theory from other session via file-path: " + quote(s))
}
if (session_base.loaded_theory(theory)) loaded_theory_node(theory)
@@ -180,7 +180,7 @@
find_theory_node(theory) match {
case Some(node_name) => node_name
case None =>
- if (Thy_Header.is_base_name(s) && literal_theory(s)) loaded_theory_node(theory)
+ if (Url.is_base_name(s) && literal_theory(s)) loaded_theory_node(theory)
else file_node(Path.explode(s).thy, dir = dir, theory = theory)
}
}
@@ -210,7 +210,7 @@
(for {
(session, (info, _)) <- sessions_structure.imports_graph.iterator
dir <- (if (session == context_session) context_dir.toList else info.dirs).iterator
- theory <- Thy_Header.try_read_dir(dir).iterator
+ theory <- Thy_Header.list_thy_names(dir).iterator
if Completion.completed(s)(theory)
} yield {
if (session == context_session || global_theory(theory)) theory
--- a/src/Pure/Thy/bibtex.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Pure/Thy/bibtex.scala Fri Dec 30 20:59:38 2022 +0000
@@ -32,7 +32,7 @@
override def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = {
val name = snapshot.node_name
if (detect(name.node)) {
- val title = "Bibliography " + quote(snapshot.node_name.path.file_name)
+ val title = "Bibliography " + quote(snapshot.node_name.file_name)
val content =
Isabelle_System.with_tmp_file("bib", "bib") { bib =>
File.write(bib, snapshot.source)
--- a/src/Pure/Thy/browser_info.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Pure/Thy/browser_info.scala Fri Dec 30 20:59:38 2022 +0000
@@ -264,7 +264,7 @@
val name = snapshot.node_name
if (plain_text) {
- val title = "File " + Symbol.cartouche_decoded(name.path.file_name)
+ val title = "File " + Symbol.cartouche_decoded(name.file_name)
val body = HTML.text(snapshot.source)
html_document(title, body, fonts_css)
}
@@ -272,7 +272,7 @@
Resources.html_document(snapshot) getOrElse {
val title =
if (name.is_theory) "Theory " + quote(name.theory_base_name)
- else "File " + Symbol.cartouche_decoded(name.path.file_name)
+ else "File " + Symbol.cartouche_decoded(name.file_name)
val xml = snapshot.xml_markup(elements = elements.html)
val body = Node_Context.empty.make_html(elements, xml)
html_document(title, body, fonts_css)
--- a/src/Pure/Thy/document_build.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Pure/Thy/document_build.scala Fri Dec 30 20:59:38 2022 +0000
@@ -140,7 +140,7 @@
def content: File.Content_XML = File.content(Path.basic(tex_name(name)), body)
def file_pos: String = name.path.implode_symbolic
def write(latex_output: Latex.Output, dir: Path): Unit =
- content.output(latex_output(_, file_pos = file_pos)).write(dir)
+ content.output(latex_output.make(_, file_pos = file_pos)).write(dir)
}
def context(
--- a/src/Pure/Thy/file_format.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Pure/Thy/file_format.scala Fri Dec 30 20:59:38 2022 +0000
@@ -80,7 +80,7 @@
name: Document.Node.Name
): Option[Document.Node.Name] = {
for {
- (_, thy) <- Thy_Header.split_file_name(name.node)
+ thy <- Url.get_base_name(name.node)
if detect(name.node) && theory_suffix.nonEmpty
}
yield {
@@ -91,9 +91,10 @@
def make_theory_content(resources: Resources, thy_name: Document.Node.Name): Option[String] = {
for {
- (prefix, suffix) <- Thy_Header.split_file_name(thy_name.node)
+ prefix <- Url.strip_base_name(thy_name.node)
+ suffix <- Url.get_base_name(thy_name.node)
if detect(prefix) && suffix == theory_suffix
- (_, thy) <- Thy_Header.split_file_name(prefix)
+ thy <- Url.get_base_name(prefix)
s <- proper_string(theory_content(thy))
} yield s
}
--- a/src/Pure/Thy/latex.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Pure/Thy/latex.scala Fri Dec 30 20:59:38 2022 +0000
@@ -158,7 +158,7 @@
else List("\\endinput\n", position(Markup.FILE, file_pos))
class Output(val options: Options) {
- def latex_output(latex_text: Text): String = apply(latex_text)
+ def latex_output(latex_text: Text): String = make(latex_text)
def latex_macro0(name: String, optional_argument: String = ""): Text =
XML.string("\\" + name + optional_argument)
@@ -214,7 +214,7 @@
error("Unknown latex markup element " + quote(elem.name) + Position.here(pos) +
":\n" + XML.string_of_tree(elem))
- def apply(latex_text: Text, file_pos: String = ""): String = {
+ def make(latex_text: Text, file_pos: String = ""): String = {
var line = 1
val result = new mutable.ListBuffer[String]
val positions = new mutable.ListBuffer[String] ++= init_position(file_pos)
--- a/src/Pure/Thy/sessions.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Pure/Thy/sessions.scala Fri Dec 30 20:59:38 2022 +0000
@@ -42,8 +42,8 @@
val file_ext = ""
override def detect(name: String): Boolean =
- Thy_Header.split_file_name(name) match {
- case Some((_, file_name)) => file_name == roots_name
+ Url.get_base_name(name) match {
+ case Some(base_name) => base_name == roots_name
case None => false
}
@@ -426,8 +426,10 @@
name <- proper_session_theories.iterator
name1 <- resources.find_theory_node(name.theory)
if name.node != name1.node
- } yield "Incoherent theory file import:\n " + name.path + " vs. \n " + name1.path)
- .toList
+ } yield {
+ "Incoherent theory file import:\n " + quote(name.node) +
+ " vs. \n " + quote(name1.node)
+ }).toList
errs1 ::: errs2 ::: errs3 ::: errs4
}
--- a/src/Pure/Thy/thy_header.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Pure/Thy/thy_header.scala Fri Dec 30 20:59:38 2022 +0000
@@ -76,32 +76,31 @@
val bootstrap_global_theories =
(Sessions.root_name :: (ml_roots ::: bootstrap_thys).map(_._2)).map(_ -> PURE)
- private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
- private val Split_File_Name = new Regex("""(.*?)[/\\]*([^/\\:]+)""")
- private val File_Name = new Regex(""".*?([^/\\:]+)""")
-
- def is_base_name(s: String): Boolean =
- s != "" && !s.exists("/\\:".contains(_))
-
- def split_file_name(s: String): Option[(String, String)] =
- s match {
- case Split_File_Name(s1, s2) => Some((s1, s2))
- case _ => None
- }
-
def import_name(s: String): String =
- s match {
- case File_Name(name) if !File.is_thy(name) => name
+ Url.get_base_name(s) match {
+ case Some(name) if !File.is_thy(name) => name
case _ => error("Malformed theory import: " + quote(s))
}
+ def get_thy_name(s: String): Option[String] = Url.get_base_name(s, suffix = ".thy")
+
+ def list_thy_names(dir: Path): List[String] = {
+ val files =
+ try { File.read_dir(dir) }
+ catch { case ERROR(_) => Nil }
+ files.flatMap(get_thy_name)
+ }
+
def theory_name(s: String): String =
- s match {
- case Thy_File_Name(name) => bootstrap_name(name)
- case File_Name(name) =>
- if (name == Sessions.root_name) name
- else ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
- case _ => ""
+ get_thy_name(s) match {
+ case Some(name) => bootstrap_name(name)
+ case None =>
+ Url.get_base_name(s) match {
+ case Some(name) =>
+ if (name == Sessions.root_name) name
+ else ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
+ case None => ""
+ }
}
def is_ml_root(theory: String): Boolean =
@@ -113,13 +112,6 @@
def bootstrap_name(theory: String): String =
bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory)
- def try_read_dir(dir: Path): List[String] = {
- val files =
- try { File.read_dir(dir) }
- catch { case ERROR(_) => Nil }
- for { Thy_File_Name(name) <- files } yield name
- }
-
/* parser */
--- a/src/Pure/Tools/build_job.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Pure/Tools/build_job.scala Fri Dec 30 20:59:38 2022 +0000
@@ -31,10 +31,8 @@
}
yield {
val master_dir =
- Thy_Header.split_file_name(thy_file) match {
- case Some((dir, _)) => dir
- case None => error("Cannot determine theory master directory: " + quote(thy_file))
- }
+ Url.strip_base_name(thy_file).getOrElse(
+ error("Cannot determine theory master directory: " + quote(thy_file)))
val node_name =
Document.Node.Name(thy_file, master_dir = master_dir, theory = theory_context.theory)
--- a/src/Tools/jEdit/src/document_model.scala Fri Dec 30 17:48:41 2022 +0000
+++ b/src/Tools/jEdit/src/document_model.scala Fri Dec 30 20:59:38 2022 +0000
@@ -314,7 +314,7 @@
PIDE.plugin.http_server.url + "/" + service.name + "?" +
(if (plain_text) plain_text_prefix else "") + Url.encode(node_name.node)
- def apply(request: HTTP.Request): Option[HTTP.Response] =
+ def apply(request: HTTP.Request): Option[HTTP.Response] = GUI_Thread.now {
for {
query <- request.decode_query
name = Library.perhaps_unprefix(plain_text_prefix, query)
@@ -331,6 +331,7 @@
fonts_css = HTML.fonts_css_dir(HTTP.url_path(request.server_name)))
HTTP.Response.html(document.content)
}
+ }
}
}