check bibtex database on ML side -- for semantic PIDE editing;
tuned signature;

--- a/src/Pure/ROOT.ML	Sun Dec 24 13:07:05 2017 +0100
+++ b/src/Pure/ROOT.ML	Sun Dec 24 14:10:41 2017 +0100
@@ -283,7 +283,6 @@
 ML_file "ML/ml_antiquotations.ML";
 ML_file "Thy/thy_output.ML";
 ML_file "Thy/document_antiquotations.ML";
-ML_file "Thy/bibtex.ML";
 ML_file "General/graph_display.ML";
 ML_file "pure_syn.ML";
 ML_file "PIDE/command.ML";
@@ -307,6 +306,7 @@
 ML_file "System/message_channel.ML";
 ML_file "System/isabelle_process.ML";
 ML_file "System/invoke_scala.ML";
+ML_file "Thy/bibtex.ML";
 ML_file "PIDE/protocol.ML";
 ML_file "General/output_primitives_virtual.ML";
 

--- a/src/Pure/Thy/bibtex.ML	Sun Dec 24 13:07:05 2017 +0100
+++ b/src/Pure/Thy/bibtex.ML	Sun Dec 24 14:10:41 2017 +0100
@@ -6,12 +6,41 @@
 
 signature BIBTEX =
 sig
+  type message = {is_error: bool, msg: string, pos: Position.T}
+  val check_database: Position.T -> string -> message list
+  val check_database_output: Position.T -> string -> unit
   val cite_macro: string Config.T
 end;
 
 structure Bibtex: BIBTEX =
 struct
 
+(* check database *)
+
+type message = {is_error: bool, msg: string, pos: Position.T};
+
+fun check_database pos0 database =
+  Invoke_Scala.method "isabelle.Bibtex.check_database_yxml" database
+  |> YXML.parse_body
+  |> let open XML.Decode in list (triple bool string properties) end
+  |> map (fn (is_error, msg, pos) =>
+      {is_error = is_error, msg = msg,
+        pos = Position.of_properties (pos @ Position.properties_of pos0)});
+
+fun check_database_output pos0 database =
+  let
+    val messages = check_database pos0 database;
+    val (errors, warnings) = List.partition #is_error messages;
+  in
+    errors |> List.app (fn {msg, pos, ...} =>
+      Output.error_message ("Bibtex error" ^ Position.here pos ^ ":\n  " ^ msg));
+    warnings |> List.app (fn {msg, pos, ...} =>
+      warning ("Bibtex warning" ^ Position.here pos ^ ":\n  " ^ msg))
+  end;
+
+
+(* document antiquotations *)
+
 val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K "cite");
 
 val _ =

--- a/src/Pure/Thy/bibtex.scala	Sun Dec 24 13:07:05 2017 +0100
+++ b/src/Pure/Thy/bibtex.scala	Sun Dec 24 14:10:41 2017 +0100
@@ -48,19 +48,17 @@
       else Output.warning("Bibtex warning" + Position.here(pos) + ":\n  " + msg)
   }
 
-  def check_database(bib_file: Path): List[Message] =
+  def check_database(database: String): List[Message] =
   {
-    val chunks = parse(Line.normalize(File.read(bib_file)))
-
+    val chunks = parse(Line.normalize(database))
+    var chunk_pos = Map.empty[String, Position.T]
     val tokens = new mutable.ListBuffer[(Token, Position.T)]
     var line = 1
     var offset = 1
-    var chunk_pos = Map.empty[String, Position.T]
-    val file_pos = bib_file.expand.position
 
     def token_pos(tok: Token): Position.T =
       Position.Offset(offset) ::: Position.End_Offset(offset + tok.source.length) :::
-      Position.Line(line) ::: file_pos
+      Position.Line(line)
 
     def advance_pos(tok: Token)
     {
@@ -116,6 +114,18 @@
     })
   }
 
+  def check_database_yxml(database: String): String =
+  {
+    val messages = check_database(database)
+
+    {
+      import XML.Encode._
+      def encode_message(message: Message): XML.Body =
+        triple(bool, string, properties)(message.is_error, message.msg, message.pos)
+      YXML.string_of_body(list[Message](encode_message _)(messages))
+    }
+  }
+
 
 
   /** document model **/