--- a/src/Pure/Isar/token.scala Fri Jan 20 20:26:42 2023 +0100
+++ b/src/Pure/Isar/token.scala Fri Jan 20 21:08:18 2023 +0100
@@ -225,7 +225,7 @@
else new Pos(line1, offset1, file, id)
}
- private def position(end_offset: Symbol.Offset): Position.T =
+ def position(end_offset: Symbol.Offset): Position.T =
(if (line > 0) Position.Line(line) else Nil) :::
(if (offset > 0) Position.Offset(offset) else Nil) :::
(if (end_offset > 0) Position.End_Offset(end_offset) else Nil) :::
--- a/src/Pure/Thy/bibtex.ML Fri Jan 20 20:26:42 2023 +0100
+++ b/src/Pure/Thy/bibtex.ML Fri Jan 20 21:08:18 2023 +0100
@@ -45,6 +45,12 @@
warning ("Unknown session context: cannot check Bibtex entry " ^
quote name ^ Position.here pos)
else ();
+ fun decode yxml =
+ let
+ val props = XML.Decode.properties (YXML.parse_body yxml);
+ val name = the_default "" (Properties.get props Markup.nameN);
+ val pos = Position.of_properties props;
+ in (name, pos) end;
in
if name = "*" then ()
else
@@ -54,7 +60,7 @@
(case \<^scala>\<open>bibtex_session_entries\<close> [id] of
[] => warn ()
| _ :: entries =>
- Completion.check_entity Markup.bibtex_entryN (map (rpair Position.none) entries)
+ Completion.check_entity Markup.bibtex_entryN (map decode entries)
ctxt (name, pos) |> ignore))
end;
--- a/src/Pure/Thy/bibtex.scala Fri Jan 20 20:26:42 2023 +0100
+++ b/src/Pure/Thy/bibtex.scala Fri Jan 20 21:08:18 2023 +0100
@@ -25,7 +25,7 @@
val file_ext: String = "bib"
override def parse_data(name: String, text: String): Bibtex.Entries =
- Bibtex.Entries.parse(text, file_pos = name)
+ Bibtex.Entries.parse(text, Isar_Token.Pos.file(name))
override def theory_suffix: String = "bibtex_file"
override def theory_content(name: String): String =
@@ -161,31 +161,33 @@
/* entries */
object Entries {
+ sealed case class Item(name: String, pos: Position.T) {
+ def encode: String = YXML.string_of_body(XML.Encode.properties(Markup.Name(name) ::: pos))
+ }
+
val empty: Entries = apply(Nil)
- def apply(entries: List[Text.Info[String]], errors: List[String] = Nil): Entries =
+ def apply(entries: List[Item], errors: List[String] = Nil): Entries =
new Entries(entries, errors)
- def parse(text: String, file_pos: String = ""): Entries = {
- val entries = new mutable.ListBuffer[Text.Info[String]]
- var offset = 0
- var line = 1
+ def parse(text: String, start: Isar_Token.Pos = Isar_Token.Pos.start): Entries = {
+ val entries = new mutable.ListBuffer[Item]
+ var pos = start
var err_line = 0
try {
for (chunk <- Bibtex.parse(text)) {
- val end_offset = offset + chunk.source.length
+ val pos1 = pos.advance(chunk.source)
if (chunk.name != "" && !chunk.is_command) {
- entries += Text.Info(Text.Range(offset, end_offset), chunk.name)
+ entries += Item(chunk.name, pos.position(pos1.offset))
}
- if (chunk.is_malformed && err_line == 0) { err_line = line }
- offset = end_offset
- line += Library.count_newlines(chunk.source)
+ if (chunk.is_malformed && err_line == 0) { err_line = pos.line }
+ pos = pos1
}
val err_pos =
- if (err_line == 0 || file_pos.isEmpty) Position.none
- else Position.Line_File(err_line, file_pos)
+ if (err_line == 0 || pos.file.isEmpty) Position.none
+ else Position.Line_File(err_line, pos.file)
val errors =
if (err_line == 0) Nil
else List("Malformed bibtex file" + Position.here(err_pos))
@@ -196,7 +198,7 @@
}
}
- final class Entries private(val entries: List[Text.Info[String]], val errors: List[String]) {
+ final class Entries private(val entries: List[Entries.Item], val errors: List[String]) {
override def toString: String = "Bibtex.Entries(" + entries.length + ")"
def ::: (other: Entries): Entries =
@@ -216,7 +218,7 @@
}
val res =
if (qualifier == Sessions.DRAFT || !sessions.defined(qualifier)) Nil
- else qualifier :: sessions(qualifier).bibtex_entries.entries.map(_.info)
+ else qualifier :: sessions(qualifier).bibtex_entries.entries.map(_.encode)
res.map(Bytes.apply)
}
}
--- a/src/Pure/Thy/sessions.scala Fri Jan 20 20:26:42 2023 +0100
+++ b/src/Pure/Thy/sessions.scala Fri Jan 20 21:08:18 2023 +0100
@@ -714,7 +714,7 @@
if File.is_bib(file.file_name)
} yield {
val path = dir + document_dir + file
- Bibtex.Entries.parse(File.read(path), file_pos = File.standard_path(path))
+ Bibtex.Entries.parse(File.read(path), start = Token.Pos.file(File.standard_path(path)))
}).foldRight(Bibtex.Entries.empty)(_ ::: _)
def record_proofs: Boolean = options.int("record_proofs") >= 2