# HG changeset patch
# User wenzelm
# Date 1674245298 -3600
# Node ID d7dc5b1e4381a3149a02c069c4b7f83ca5602f97
# Parent  1046a69fabaa55ca9f039efa6d9b6a30d6265553
proper positions for Isabelle/ML, instead of Isabelle/Scala;

diff -r 1046a69fabaa -r d7dc5b1e4381 src/Pure/Isar/token.scala
--- 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) :::
diff -r 1046a69fabaa -r d7dc5b1e4381 src/Pure/Thy/bibtex.ML
--- 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;
 
diff -r 1046a69fabaa -r d7dc5b1e4381 src/Pure/Thy/bibtex.scala
--- 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)
     }
   }
diff -r 1046a69fabaa -r d7dc5b1e4381 src/Pure/Thy/sessions.scala
--- 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