# HG changeset patch # User paulson # Date 1672433978 0 # Node ID 6be3459fc4c1c26ca97071ab562ef778cf07e177 # Parent 72daee8a39cad989e75aee1835297e4bf3b9af07# Parent ab08604729a2e1c75fca89525ddf10bd9326c8d2 merged diff -r ab08604729a2 -r 6be3459fc4c1 src/Pure/Admin/check_sources.scala --- 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")) diff -r ab08604729a2 -r 6be3459fc4c1 src/Pure/General/path.scala --- 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 */ diff -r ab08604729a2 -r 6be3459fc4c1 src/Pure/General/url.scala --- 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, ".") diff -r ab08604729a2 -r 6be3459fc4c1 src/Pure/PIDE/command.scala --- 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) diff -r ab08604729a2 -r 6be3459fc4c1 src/Pure/PIDE/document.scala --- 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)) diff -r ab08604729a2 -r 6be3459fc4c1 src/Pure/PIDE/line.scala --- 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) } } diff -r ab08604729a2 -r 6be3459fc4c1 src/Pure/PIDE/resources.scala --- 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 diff -r ab08604729a2 -r 6be3459fc4c1 src/Pure/Thy/bibtex.scala --- 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) diff -r ab08604729a2 -r 6be3459fc4c1 src/Pure/Thy/browser_info.scala --- 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) diff -r ab08604729a2 -r 6be3459fc4c1 src/Pure/Thy/document_build.scala --- 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( diff -r ab08604729a2 -r 6be3459fc4c1 src/Pure/Thy/file_format.scala --- 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 } diff -r ab08604729a2 -r 6be3459fc4c1 src/Pure/Thy/latex.scala --- 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) diff -r ab08604729a2 -r 6be3459fc4c1 src/Pure/Thy/sessions.scala --- 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 } diff -r ab08604729a2 -r 6be3459fc4c1 src/Pure/Thy/thy_header.scala --- 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 */ diff -r ab08604729a2 -r 6be3459fc4c1 src/Pure/Tools/build_job.scala --- 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) diff -r ab08604729a2 -r 6be3459fc4c1 src/Tools/jEdit/src/document_model.scala --- 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) } + } } }