# HG changeset patch
# User wenzelm
# Date 1514573623 -3600
# Node ID e255c76db0525f1ee783bde108b51edd855fc2fb
# Parent  0bfbf5b9d6ba0deda94310d733070777b1bcab6a
clarified signature;

diff -r 0bfbf5b9d6ba -r e255c76db052 src/Pure/Thy/bibtex.ML
--- a/src/Pure/Thy/bibtex.ML	Fri Dec 29 19:35:26 2017 +0100
+++ b/src/Pure/Thy/bibtex.ML	Fri Dec 29 19:53:43 2017 +0100
@@ -6,8 +6,8 @@
 
 signature BIBTEX =
 sig
-  type message = {is_error: bool, msg: string, pos: Position.T}
-  val check_database: Position.T -> string -> message list
+  val check_database:
+    Position.T -> string -> (string * Position.T) list * (string * Position.T) list
   val check_database_output: Position.T -> string -> unit
   val cite_macro: string Config.T
 end;
@@ -17,23 +17,19 @@
 
 (* check database *)
 
-type message = {is_error: bool, msg: string, pos: Position.T};
+type message = string * 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.get_props pos0)});
+  |> let open XML.Decode in pair (list (pair string properties)) (list (pair string properties)) end
+  |> (apply2 o map o apsnd) (fn pos => Position.of_properties (pos @ Position.get_props 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, ...} =>
+  let val (errors, warnings) = check_database pos0 database in
+    errors |> List.app (fn (msg, pos) =>
       Output.error_message ("Bibtex error" ^ Position.here pos ^ ":\n  " ^ msg));
-    warnings |> List.app (fn {msg, pos, ...} =>
+    warnings |> List.app (fn (msg, pos) =>
       warning ("Bibtex warning" ^ Position.here pos ^ ":\n  " ^ msg))
   end;
 
diff -r 0bfbf5b9d6ba -r e255c76db052 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Fri Dec 29 19:35:26 2017 +0100
+++ b/src/Pure/Thy/bibtex.scala	Fri Dec 29 19:53:43 2017 +0100
@@ -44,15 +44,7 @@
 
   /** check database **/
 
-  sealed case class Message(is_error: Boolean, msg: String, pos: Position.T)
-  {
-    def output: Unit =
-      if (is_error)
-        Output.error_message("Bibtex error" + Position.here(pos) + ":\n  " + msg)
-      else Output.warning("Bibtex warning" + Position.here(pos) + ":\n  " + msg)
-  }
-
-  def check_database(database: String): List[Message] =
+  def check_database(database: String): (List[(String, Position.T)], List[(String, Position.T)]) =
   {
     val chunks = parse(Line.normalize(database))
     var chunk_pos = Map.empty[String, Position.T]
@@ -101,32 +93,29 @@
       val log_file = tmp_dir + Path.explode("root.blg")
       val lines = if (log_file.is_file) Line.logical_lines(File.read(log_file)) else Nil
 
-      lines.zip(lines.tail ::: List("")).flatMap(
-        {
-          case (Error(msg, Value.Int(l)), _) =>
-            Some(Message(true, msg, get_line_pos(l)))
-          case (Warning_in_Chunk(msg, name), _) if chunk_pos.isDefinedAt(name) =>
-            Some(Message(false, Word.capitalize(msg + " in entry " + quote(name)), chunk_pos(name)))
-          case (Warning(msg), Warning_Line(Value.Int(l))) =>
-            Some(Message(false, Word.capitalize(msg), get_line_pos(l)))
-          case (Warning(msg), _) =>
-            Some(Message(false, Word.capitalize(msg), Position.none))
-          case _ => None
-        }
-      )
+      val (errors, warnings) =
+        lines.zip(lines.tail ::: List("")).flatMap(
+          {
+            case (Error(msg, Value.Int(l)), _) =>
+              Some((true, (msg, get_line_pos(l))))
+            case (Warning_in_Chunk(msg, name), _) if chunk_pos.isDefinedAt(name) =>
+              Some((false, (Word.capitalize(msg + " in entry " + quote(name)), chunk_pos(name))))
+            case (Warning(msg), Warning_Line(Value.Int(l))) =>
+              Some((false, (Word.capitalize(msg), get_line_pos(l))))
+            case (Warning(msg), _) =>
+              Some((false, (Word.capitalize(msg), Position.none)))
+            case _ => None
+          }
+        ).partition(_._1)
+      (errors.map(_._2), warnings.map(_._2))
     })
   }
 
   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))
-    }
+    import XML.Encode._
+    YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))(
+      check_database(database)))
   }