--- 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;
--- 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)))
}