--- a/etc/build.props Sat Jan 20 15:07:41 2024 +0100
+++ b/etc/build.props Sat Jan 20 16:09:35 2024 +0100
@@ -77,6 +77,7 @@
src/Pure/GUI/wrap_panel.scala \
src/Pure/General/antiquote.scala \
src/Pure/General/base64.scala \
+ src/Pure/General/bibtex.scala \
src/Pure/General/bytes.scala \
src/Pure/General/cache.scala \
src/Pure/General/codepoint.scala \
@@ -96,6 +97,7 @@
src/Pure/General/js.scala \
src/Pure/General/json.scala \
src/Pure/General/json_api.scala \
+ src/Pure/General/latex.scala \
src/Pure/General/linear_set.scala \
src/Pure/General/logger.scala \
src/Pure/General/long_name.scala \
@@ -191,9 +193,7 @@
src/Pure/System/scala.scala \
src/Pure/System/system_channel.scala \
src/Pure/System/tty_loop.scala \
- src/Pure/Thy/bibtex.scala \
src/Pure/Thy/document_build.scala \
- src/Pure/Thy/latex.scala \
src/Pure/Thy/thy_element.scala \
src/Pure/Thy/thy_header.scala \
src/Pure/Thy/thy_syntax.scala \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/bibtex.ML Sat Jan 20 16:09:35 2024 +0100
@@ -0,0 +1,134 @@
+(* Title: Pure/General/bibtex.ML
+ Author: Makarius
+
+Support for BibTeX.
+*)
+
+signature BIBTEX =
+sig
+ val check_database:
+ Position.T -> string -> (string * Position.T) list * (string * Position.T) list
+ val check_database_output: Position.T -> string -> unit
+ val check_bibtex_entry: Proof.context -> string * Position.T -> unit
+ val cite_macro: string Config.T
+ val cite_antiquotation: binding -> (Proof.context -> string) -> theory -> theory
+end;
+
+structure Bibtex: BIBTEX =
+struct
+
+(* check database *)
+
+type message = string * Position.T;
+
+fun check_database pos0 database =
+ \<^scala>\<open>bibtex_check_database\<close> database
+ |> YXML.parse_body
+ |> 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.properties_of pos0));
+
+fun check_database_output pos0 database =
+ 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) =>
+ warning ("Bibtex warning" ^ Position.here pos ^ ":\n " ^ msg))
+ end;
+
+
+(* check bibtex entry *)
+
+fun check_bibtex_entry ctxt (name, pos) =
+ let
+ fun warn () =
+ if Context_Position.is_visible ctxt then
+ 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 = Properties.get_string props Markup.nameN;
+ val pos = Position.of_properties props;
+ in (name, pos) end;
+ in
+ if name = "*" then ()
+ else
+ (case Position.id_of pos of
+ NONE => warn ()
+ | SOME id =>
+ (case \<^scala>\<open>bibtex_session_entries\<close> [id] of
+ [] => warn ()
+ | _ :: entries =>
+ Completion.check_entity Markup.bibtex_entryN (map decode entries)
+ ctxt (name, pos) |> ignore))
+ end;
+
+
+(* document antiquotations *)
+
+val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K "");
+fun get_cite_macro ctxt = Config.get ctxt cite_macro;
+
+val _ =
+ Theory.setup (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro));
+
+
+local
+
+val parse_citations = Parse.and_list1 (Parse.position Parse.name);
+
+fun cite_command ctxt get_kind ((opt_loc, citations), macro_name) =
+ let
+ val loc = the_default Input.empty opt_loc;
+ val _ = Context_Position.reports ctxt (Document_Output.document_reports loc);
+ val _ = List.app (check_bibtex_entry ctxt) citations;
+
+ val kind = if macro_name = "" then get_kind ctxt else macro_name;
+ val location = Document_Output.output_document ctxt {markdown = false} loc;
+ in Latex.cite {kind = kind, citations = citations, location = location} end;
+
+fun cite_command_old ctxt get_kind args =
+ let
+ val _ =
+ if Context_Position.is_visible ctxt then
+ legacy_feature ("Old antiquotation syntax, better use \"isabelle update -u cite\"" ^
+ Position.here_list (map snd (snd args)))
+ else ();
+ in cite_command ctxt get_kind (args, "") end;
+
+val cite_keywords =
+ Thy_Header.bootstrap_keywords
+ |> Keyword.add_keywords (map (fn a => ((a, Position.none), Keyword.no_spec)) ["in", "using"]);
+
+fun cite_command_embedded ctxt get_kind input =
+ let
+ val parser =
+ Scan.option (Parse.embedded_input --| Parse.$$$ "in") -- parse_citations --
+ Scan.optional (Parse.$$$ "using" |-- Parse.!!! Parse.name) "";
+ val args = Parse.read_embedded ctxt cite_keywords parser input;
+ in cite_command ctxt get_kind args end;
+
+fun cite_command_parser get_kind =
+ Scan.option Args.cartouche_input -- parse_citations
+ >> (fn args => fn ctxt => cite_command_old ctxt get_kind args) ||
+ Parse.embedded_input
+ >> (fn arg => fn ctxt => cite_command_embedded ctxt get_kind arg);
+
+in
+
+fun cite_antiquotation binding get_kind =
+ Document_Output.antiquotation_raw binding (Scan.lift (cite_command_parser get_kind))
+ (fn ctxt => fn cmd => cmd ctxt);
+
+end;
+
+val _ =
+ Theory.setup
+ (cite_antiquotation \<^binding>\<open>cite\<close> get_cite_macro #>
+ cite_antiquotation \<^binding>\<open>nocite\<close> (K "nocite") #>
+ cite_antiquotation \<^binding>\<open>citet\<close> (K "citet") #>
+ cite_antiquotation \<^binding>\<open>citep\<close> (K "citep"));
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/bibtex.scala Sat Jan 20 16:09:35 2024 +0100
@@ -0,0 +1,855 @@
+/* Title: Pure/General/bibtex.scala
+ Author: Makarius
+
+Support for BibTeX.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+
+import scala.collection.mutable
+import scala.util.parsing.combinator.RegexParsers
+import scala.util.parsing.input.Reader
+import scala.util.matching.Regex
+
+import isabelle.{Token => Isar_Token}
+
+
+object Bibtex {
+ /** file format **/
+
+ class File_Format extends isabelle.File_Format {
+ val format_name: String = "bibtex"
+ val file_ext: String = "bib"
+
+ override def parse_data(name: String, text: String): Bibtex.Entries =
+ Bibtex.Entries.parse(text, Isar_Token.Pos.file(name))
+
+ override def theory_suffix: String = "bibtex_file"
+ override def theory_content(name: String): String =
+ """theory "bib" imports Pure begin bibtex_file "." end"""
+ override def theory_excluded(name: String): Boolean = name == "bib"
+
+ override def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = {
+ val name = snapshot.node_name
+ if (detect(name.node)) {
+ val title = "Bibliography " + quote(snapshot.node_name.file_name)
+ val content =
+ Isabelle_System.with_tmp_file("bib", "bib") { bib =>
+ File.write(bib, snapshot.node.source)
+ Bibtex.html_output(List(bib), style = "unsort", title = title)
+ }
+ Some(Browser_Info.HTML_Document(title, content))
+ }
+ else None
+ }
+ }
+
+
+
+ /** bibtex errors **/
+
+ def bibtex_errors(dir: Path, root_name: String): List[String] = {
+ val log_path = dir + Path.explode(root_name).blg
+ if (log_path.is_file) {
+ val Error1 = """^(I couldn't open database file .+)$""".r
+ val Error2 = """^(I found no .+)$""".r
+ val Error3 = """^(.+)---line (\d+) of file (.+)""".r
+ Line.logical_lines(File.read(log_path)).flatMap(line =>
+ line match {
+ case Error1(msg) => Some("Bibtex error: " + msg)
+ case Error2(msg) => Some("Bibtex error: " + msg)
+ case Error3(msg, Value.Int(l), file) =>
+ val path = File.standard_path(file)
+ if (Path.is_wellformed(path)) {
+ val pos = Position.Line_File(l, (dir + Path.explode(path)).canonical.implode)
+ Some("Bibtex error" + Position.here(pos) + ":\n " + msg)
+ }
+ else None
+ case _ => None
+ })
+ }
+ else Nil
+ }
+
+
+
+ /** check database **/
+
+ 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]
+ val tokens = new mutable.ListBuffer[(Token, Position.T)]
+ var line = 1
+ var offset = 1
+
+ def make_pos(length: Int): Position.T =
+ Position.Offset(offset) ::: Position.End_Offset(offset + length) ::: Position.Line(line)
+
+ def advance_pos(tok: Token): Unit = {
+ for (s <- Symbol.iterator(tok.source)) {
+ if (Symbol.is_newline(s)) line += 1
+ offset += 1
+ }
+ }
+
+ def get_line_pos(l: Int): Position.T =
+ if (0 < l && l <= tokens.length) tokens(l - 1)._2 else Position.none
+
+ for (chunk <- chunks) {
+ val name = chunk.name
+ if (name != "" && !chunk_pos.isDefinedAt(name)) {
+ chunk_pos += (name -> make_pos(chunk.heading_length))
+ }
+ for (tok <- chunk.tokens) {
+ tokens += (tok.copy(source = tok.source.replace("\n", " ")) -> make_pos(tok.source.length))
+ advance_pos(tok)
+ }
+ }
+
+ Isabelle_System.with_tmp_dir("bibtex") { tmp_dir =>
+ File.write(tmp_dir + Path.explode("root.bib"),
+ tokens.iterator.map(p => p._1.source).mkString("", "\n", "\n"))
+ File.write(tmp_dir + Path.explode("root.aux"),
+ "\\bibstyle{plain}\n\\bibdata{root}\n\\citation{*}")
+ Isabelle_System.bash("\"$ISABELLE_BIBTEX\" root", cwd = tmp_dir.file)
+
+ val Error = """^(.*)---line (\d+) of file root.bib$""".r
+ val Warning = """^Warning--(.+)$""".r
+ val Warning_Line = """--line (\d+) of file root.bib$""".r
+ val Warning_in_Chunk = """^Warning--(.+) in (.+)$""".r
+
+ 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
+
+ val (errors, warnings) =
+ if (lines.isEmpty) (Nil, Nil)
+ else {
+ 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.capitalized(msg) + " in entry " + quote(name), chunk_pos(name))))
+ case (Warning(msg), Warning_Line(Value.Int(l))) =>
+ Some((false, (Word.capitalized(msg), get_line_pos(l))))
+ case (Warning(msg), _) =>
+ Some((false, (Word.capitalized(msg), Position.none)))
+ case _ => None
+ }
+ ).partition(_._1)
+ }
+ (errors.map(_._2), warnings.map(_._2))
+ }
+ }
+
+ object Check_Database extends Scala.Fun_String("bibtex_check_database") {
+ val here = Scala_Project.here
+ def apply(database: String): String = {
+ import XML.Encode._
+ YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))(
+ check_database(database)))
+ }
+ }
+
+
+
+ /** document model **/
+
+ /* entries */
+
+ sealed case class Entry(name: String, pos: Position.T) {
+ def encode: String = YXML.string_of_body(XML.Encode.properties(Markup.Name(name) ::: pos))
+ }
+
+ object Entries {
+ val empty: Entries = apply(Nil)
+
+ def apply(entries: List[Entry], errors: List[String] = Nil): Entries =
+ new Entries(entries, errors)
+
+ def parse(text: String, start: Isar_Token.Pos = Isar_Token.Pos.start): Entries = {
+ val entries = new mutable.ListBuffer[Entry]
+ var pos = start
+ var err_line = 0
+
+ try {
+ for (chunk <- Bibtex.parse(text)) {
+ val pos1 = pos.advance(chunk.source)
+ if (chunk.name != "" && !chunk.is_command) {
+ entries += Entry(chunk.name, pos.position(pos1.offset))
+ }
+ if (chunk.is_malformed && err_line == 0) { err_line = pos.line }
+ pos = pos1
+ }
+
+ val err_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))
+
+ apply(entries.toList, errors = errors)
+ }
+ catch { case ERROR(msg) => apply(Nil, errors = List(msg)) }
+ }
+ }
+
+ final class Entries private(val entries: List[Entry], val errors: List[String]) {
+ override def toString: String = "Bibtex.Entries(" + entries.length + ")"
+
+ def ::: (other: Entries): Entries =
+ new Entries(other.entries ::: entries, other.errors ::: errors)
+ }
+
+ object Session_Entries extends Scala.Fun("bibtex_session_entries") {
+ val here = Scala_Project.here
+
+ override def invoke(session: Session, args: List[Bytes]): List[Bytes] = {
+ val sessions = session.resources.sessions_structure
+ val id = Value.Long.parse(Library.the_single(args).text)
+ val qualifier =
+ session.get_state().lookup_id(id) match {
+ case None => Sessions.DRAFT
+ case Some(st) => sessions.theory_qualifier(st.command.node_name.theory)
+ }
+ val res =
+ if (qualifier == Sessions.DRAFT || !sessions.defined(qualifier)) Nil
+ else qualifier :: sessions(qualifier).bibtex_entries.entries.map(_.encode)
+ res.map(Bytes.apply)
+ }
+ }
+
+
+
+ /** content **/
+
+ private val months = List(
+ "jan",
+ "feb",
+ "mar",
+ "apr",
+ "may",
+ "jun",
+ "jul",
+ "aug",
+ "sep",
+ "oct",
+ "nov",
+ "dec")
+ def is_month(s: String): Boolean = months.contains(s.toLowerCase)
+
+ private val commands = List("preamble", "string")
+ def is_command(s: String): Boolean = commands.contains(s.toLowerCase)
+
+ sealed case class Entry_Type(
+ kind: String,
+ required: List[String],
+ optional_crossref: List[String],
+ optional_other: List[String]
+ ) {
+ val optional_standard: List[String] = List("url", "doi", "ee")
+
+ def is_required(s: String): Boolean = required.contains(s.toLowerCase)
+ def is_optional(s: String): Boolean =
+ optional_crossref.contains(s.toLowerCase) ||
+ optional_other.contains(s.toLowerCase) ||
+ optional_standard.contains(s.toLowerCase)
+
+ def fields: List[String] =
+ required ::: optional_crossref ::: optional_other ::: optional_standard
+
+ def template: String =
+ "@" + kind + "{,\n" + fields.map(x => " " + x + " = {},\n").mkString + "}\n"
+ }
+
+ val known_entries: List[Entry_Type] =
+ List(
+ Entry_Type("Article",
+ List("author", "title"),
+ List("journal", "year"),
+ List("volume", "number", "pages", "month", "note")),
+ Entry_Type("InProceedings",
+ List("author", "title"),
+ List("booktitle", "year"),
+ List("editor", "volume", "number", "series", "pages", "month", "address",
+ "organization", "publisher", "note")),
+ Entry_Type("InCollection",
+ List("author", "title", "booktitle"),
+ List("publisher", "year"),
+ List("editor", "volume", "number", "series", "type", "chapter", "pages",
+ "edition", "month", "address", "note")),
+ Entry_Type("InBook",
+ List("author", "editor", "title", "chapter"),
+ List("publisher", "year"),
+ List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")),
+ Entry_Type("Proceedings",
+ List("title", "year"),
+ List(),
+ List("booktitle", "editor", "volume", "number", "series", "address", "month",
+ "organization", "publisher", "note")),
+ Entry_Type("Book",
+ List("author", "editor", "title"),
+ List("publisher", "year"),
+ List("volume", "number", "series", "address", "edition", "month", "note")),
+ Entry_Type("Booklet",
+ List("title"),
+ List(),
+ List("author", "howpublished", "address", "month", "year", "note")),
+ Entry_Type("PhdThesis",
+ List("author", "title", "school", "year"),
+ List(),
+ List("type", "address", "month", "note")),
+ Entry_Type("MastersThesis",
+ List("author", "title", "school", "year"),
+ List(),
+ List("type", "address", "month", "note")),
+ Entry_Type("TechReport",
+ List("author", "title", "institution", "year"),
+ List(),
+ List("type", "number", "address", "month", "note")),
+ Entry_Type("Manual",
+ List("title"),
+ List(),
+ List("author", "organization", "address", "edition", "month", "year", "note")),
+ Entry_Type("Unpublished",
+ List("author", "title", "note"),
+ List(),
+ List("month", "year")),
+ Entry_Type("Misc",
+ List(),
+ List(),
+ List("author", "title", "howpublished", "month", "year", "note")))
+
+ def known_entry(kind: String): Option[Entry_Type] =
+ known_entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase)
+
+
+
+ /** tokens and chunks **/
+
+ object Token {
+ object Kind extends Enumeration {
+ val COMMAND = Value("command")
+ val ENTRY = Value("entry")
+ val KEYWORD = Value("keyword")
+ val NAT = Value("natural number")
+ val STRING = Value("string")
+ val NAME = Value("name")
+ val IDENT = Value("identifier")
+ val SPACE = Value("white space")
+ val COMMENT = Value("ignored text")
+ val ERROR = Value("bad input")
+ }
+ }
+
+ sealed case class Token(kind: Token.Kind.Value, source: String) {
+ def is_kind: Boolean =
+ kind == Token.Kind.COMMAND ||
+ kind == Token.Kind.ENTRY ||
+ kind == Token.Kind.IDENT
+ def is_name: Boolean =
+ kind == Token.Kind.NAME ||
+ kind == Token.Kind.IDENT
+ def is_ignored: Boolean =
+ kind == Token.Kind.SPACE ||
+ kind == Token.Kind.COMMENT
+ def is_malformed: Boolean =
+ kind == Token.Kind.ERROR
+ def is_open: Boolean =
+ kind == Token.Kind.KEYWORD && (source == "{" || source == "(")
+ }
+
+ case class Chunk(kind: String, tokens: List[Token]) {
+ val source: String = tokens.map(_.source).mkString
+
+ private val content: Option[List[Token]] =
+ tokens match {
+ case Token(Token.Kind.KEYWORD, "@") :: body if body.nonEmpty =>
+ (body.init.filterNot(_.is_ignored), body.last) match {
+ case (tok :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}"))
+ if tok.is_kind => Some(toks)
+
+ case (tok :: Token(Token.Kind.KEYWORD, "(") :: toks, Token(Token.Kind.KEYWORD, ")"))
+ if tok.is_kind => Some(toks)
+
+ case _ => None
+ }
+ case _ => None
+ }
+
+ def name: String =
+ content match {
+ case Some(tok :: _) if tok.is_name => tok.source
+ case _ => ""
+ }
+
+ def heading_length: Int =
+ if (name == "") 1
+ else {
+ tokens.takeWhile(tok => !tok.is_open).foldLeft(0) { case (n, tok) => n + tok.source.length }
+ }
+
+ def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
+ def is_malformed: Boolean = tokens.exists(_.is_malformed)
+ def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined
+ def is_entry: Boolean = Bibtex.known_entry(kind).isDefined && name != "" && content.isDefined
+ }
+
+
+
+ /** parsing **/
+
+ // context of partial line-oriented scans
+ abstract class Line_Context
+ case object Ignored extends Line_Context
+ case object At extends Line_Context
+ case class Item_Start(kind: String) extends Line_Context
+ case class Item_Open(kind: String, end: String) extends Line_Context
+ case class Item(kind: String, end: String, delim: Delimited) extends Line_Context
+
+ case class Delimited(quoted: Boolean, depth: Int)
+ val Closed: Delimited = Delimited(false, 0)
+
+ private def token(kind: Token.Kind.Value)(source: String): Token = Token(kind, source)
+ private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source)
+
+
+ // See also https://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web
+ // module @<Scan for and process a \.{.bib} command or database entry@>.
+
+ object Parsers extends RegexParsers {
+ /* white space and comments */
+
+ override val whiteSpace = "".r
+
+ private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE)
+ private val spaces = rep(space)
+
+
+ /* ignored text */
+
+ private val ignored: Parser[Chunk] =
+ rep1("""(?i)([^@]+|@[ \t]*comment)""".r) ^^ {
+ case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) }
+
+ private def ignored_line: Parser[(Chunk, Line_Context)] =
+ ignored ^^ { case a => (a, Ignored) }
+
+
+ /* delimited string: outermost "..." or {...} and body with balanced {...} */
+
+ // see also bibtex.web: scan_a_field_token_and_eat_white, scan_balanced_braces
+ private def delimited_depth(delim: Delimited): Parser[(String, Delimited)] =
+ new Parser[(String, Delimited)] {
+ require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0,
+ "bad delimiter depth")
+
+ def apply(in: Input): ParseResult[(String, Delimited)] = {
+ val start = in.offset
+ val end = in.source.length
+
+ var i = start
+ var q = delim.quoted
+ var d = delim.depth
+ var finished = false
+ while (!finished && i < end) {
+ val c = in.source.charAt(i)
+
+ if (c == '"' && d == 0) { i += 1; d = 1; q = true }
+ else if (c == '"' && d == 1 && q) {
+ i += 1; d = 0; q = false; finished = true
+ }
+ else if (c == '{') { i += 1; d += 1 }
+ else if (c == '}') {
+ if (d == 1 && !q || d > 1) { i += 1; d -= 1; if (d == 0) finished = true }
+ else {i = start; finished = true }
+ }
+ else if (d > 0) i += 1
+ else finished = true
+ }
+ if (i == start) Failure("bad input", in)
+ else {
+ val s = in.source.subSequence(start, i).toString
+ Success((s, Delimited(q, d)), in.drop(i - start))
+ }
+ }
+ }.named("delimited_depth")
+
+ private def delimited: Parser[Token] =
+ delimited_depth(Closed) ^?
+ { case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) }
+
+ private def recover_delimited: Parser[Token] =
+ """["{][^@]*""".r ^^ token(Token.Kind.ERROR)
+
+ def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] =
+ delimited_depth(ctxt.delim) ^^ { case (s, delim1) =>
+ (Chunk(ctxt.kind, List(Token(Token.Kind.STRING, s))), ctxt.copy(delim = delim1)) } |
+ recover_delimited ^^ { case a => (Chunk(ctxt.kind, List(a)), Ignored) }
+
+
+ /* other tokens */
+
+ private val at = "@" ^^ keyword
+
+ private val nat = "[0-9]+".r ^^ token(Token.Kind.NAT)
+
+ private val name = """[\x21-\x7f&&[^"#%'(),={}]]+""".r ^^ token(Token.Kind.NAME)
+
+ private val identifier =
+ """[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r
+
+ private val ident = identifier ^^ token(Token.Kind.IDENT)
+
+ val other_token: Parser[Token] = "[=#,]".r ^^ keyword | (nat | (ident | space))
+
+
+ /* body */
+
+ private val body =
+ delimited | (recover_delimited | other_token)
+
+ private def body_line(ctxt: Item) =
+ if (ctxt.delim.depth > 0)
+ delimited_line(ctxt)
+ else
+ delimited_line(ctxt) |
+ other_token ^^ { case a => (Chunk(ctxt.kind, List(a)), ctxt) } |
+ ctxt.end ^^ { case a => (Chunk(ctxt.kind, List(keyword(a))), Ignored) }
+
+
+ /* items: command or entry */
+
+ private val item_kind =
+ identifier ^^ { case a =>
+ val kind =
+ if (is_command(a)) Token.Kind.COMMAND
+ else if (known_entry(a).isDefined) Token.Kind.ENTRY
+ else Token.Kind.IDENT
+ Token(kind, a)
+ }
+
+ private val item_begin =
+ "{" ^^ { case a => ("}", keyword(a)) } |
+ "(" ^^ { case a => (")", keyword(a)) }
+
+ private def item_name(kind: String) =
+ kind.toLowerCase match {
+ case "preamble" => failure("")
+ case "string" => identifier ^^ token(Token.Kind.NAME)
+ case _ => name
+ }
+
+ private val item_start =
+ at ~ spaces ~ item_kind ~ spaces ^^
+ { case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) }
+
+ private val item: Parser[Chunk] =
+ (item_start ~ item_begin ~ spaces) into
+ { case (kind, a) ~ ((end, b)) ~ c =>
+ opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ {
+ case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } }
+
+ private val recover_item: Parser[Chunk] =
+ at ~ "[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) }
+
+
+ /* chunks */
+
+ val chunk: Parser[Chunk] = ignored | (item | recover_item)
+
+ def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] = {
+ ctxt match {
+ case Ignored =>
+ ignored_line |
+ at ^^ { case a => (Chunk("", List(a)), At) }
+
+ case At =>
+ space ^^ { case a => (Chunk("", List(a)), ctxt) } |
+ item_kind ^^ { case a => (Chunk(a.source, List(a)), Item_Start(a.source)) } |
+ recover_item ^^ { case a => (a, Ignored) } |
+ ignored_line
+
+ case Item_Start(kind) =>
+ space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
+ item_begin ^^ { case (end, a) => (Chunk(kind, List(a)), Item_Open(kind, end)) } |
+ recover_item ^^ { case a => (a, Ignored) } |
+ ignored_line
+
+ case Item_Open(kind, end) =>
+ space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
+ item_name(kind) ^^ { case a => (Chunk(kind, List(a)), Item(kind, end, Closed)) } |
+ body_line(Item(kind, end, Closed)) |
+ ignored_line
+
+ case item_ctxt: Item =>
+ body_line(item_ctxt) |
+ ignored_line
+
+ case _ => failure("")
+ }
+ }
+ }
+
+
+ /* parse */
+
+ def parse(input: CharSequence): List[Chunk] =
+ Parsers.parseAll(Parsers.rep(Parsers.chunk), Scan.char_reader(input)) match {
+ case Parsers.Success(result, _) => result
+ case _ => error("Unexpected failure to parse input:\n" + input.toString)
+ }
+
+ def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) = {
+ var in: Reader[Char] = Scan.char_reader(input)
+ val chunks = new mutable.ListBuffer[Chunk]
+ var ctxt = context
+ while (!in.atEnd) {
+ val result = Parsers.parse(Parsers.chunk_line(ctxt), in)
+ (result : @unchecked) match {
+ case Parsers.Success((x, c), rest) => chunks += x; ctxt = c; in = rest
+ case Parsers.NoSuccess(_, rest) =>
+ error("Unepected failure to parse input:\n" + rest.source.toString)
+ }
+ }
+ (chunks.toList, ctxt)
+ }
+
+
+
+ /** HTML output **/
+
+ private val output_styles =
+ List(
+ "" -> "html-n",
+ "plain" -> "html-n",
+ "alpha" -> "html-a",
+ "named" -> "html-n",
+ "paragraph" -> "html-n",
+ "unsort" -> "html-u",
+ "unsortlist" -> "html-u")
+
+ def html_output(bib: List[Path],
+ title: String = "Bibliography",
+ body: Boolean = false,
+ citations: List[String] = List("*"),
+ style: String = "",
+ chronological: Boolean = false
+ ): String = {
+ Isabelle_System.with_tmp_dir("bibtex") { tmp_dir =>
+ /* database files */
+
+ val bib_files = bib.map(_.drop_ext)
+ val bib_names = {
+ val names0 = bib_files.map(_.file_name)
+ if (Library.duplicates(names0).isEmpty) names0
+ else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name })
+ }
+
+ for ((a, b) <- bib_files zip bib_names) {
+ Isabelle_System.copy_file(a.bib, tmp_dir + Path.basic(b).bib)
+ }
+
+
+ /* style file */
+
+ val bst =
+ output_styles.toMap.get(style) match {
+ case Some(base) => base + (if (chronological) "c" else "") + ".bst"
+ case None =>
+ error("Bad style for bibtex HTML output: " + quote(style) +
+ "\n(expected: " + commas_quote(output_styles.map(_._1)) + ")")
+ }
+ Isabelle_System.copy_file(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir)
+
+
+ /* result */
+
+ val in_file = Path.explode("bib.aux")
+ val out_file = Path.explode("bib.html")
+
+ File.write(tmp_dir + in_file,
+ bib_names.mkString("\\bibdata{", ",", "}\n") +
+ citations.map(cite => "\\citation{" + cite + "}\n").mkString)
+
+ Isabelle_System.bash(
+ "\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" +
+ " -u -s " + Bash.string(proper_string(style) getOrElse "empty") +
+ (if (chronological) " -c" else "") +
+ if_proper(title, " -h " + Bash.string(title) + " ") +
+ " " + File.bash_path(in_file) + " " + File.bash_path(out_file),
+ cwd = tmp_dir.file).check
+
+ val html = File.read(tmp_dir + out_file)
+
+ if (body) {
+ cat_lines(
+ split_lines(html).
+ dropWhile(line => !line.startsWith("<!-- BEGIN BIBLIOGRAPHY")).reverse.
+ dropWhile(line => !line.startsWith("<!-- END BIBLIOGRAPHY")).reverse)
+ }
+ else html
+ }
+ }
+
+
+
+ /** cite commands and antiquotations **/
+
+ /* cite commands */
+
+ def cite_commands(options: Options): List[String] =
+ space_explode(',', options.string("document_cite_commands"))
+
+ val CITE = "cite"
+ val NOCITE = "nocite"
+
+
+ /* citations within theory source */
+
+ object Cite {
+ def unapply(tree: XML.Tree): Option[Inner] =
+ tree match {
+ case XML.Elem(Markup(Markup.Latex_Cite.name, props), body) =>
+ val kind = Markup.Kind.unapply(props).getOrElse(CITE)
+ val citations = Markup.Citations.get(props)
+ val pos = props.filter(Markup.position_property)
+ Some(Inner(kind, citations, body, pos))
+ case _ => None
+ }
+
+ sealed case class Inner(kind: String, citations: String, location: XML.Body, pos: Position.T) {
+ def nocite: Inner = copy(kind = NOCITE, location = Nil)
+
+ def latex_text: Latex.Text = {
+ val props =
+ (if (kind.nonEmpty) Markup.Kind(kind) else Nil) :::
+ Markup.Citations(citations) ::: pos
+ List(XML.Elem(Markup.Latex_Cite(props), location))
+ }
+
+ override def toString: String = citations
+ }
+
+ sealed case class Outer(kind: String, body: String, start: Isar_Token.Pos) {
+ def pos: Position.T = start.position()
+
+ def parse: Option[Inner] = {
+ val tokens = Isar_Token.explode(Parsers.keywords, body)
+ Parsers.parse_all(Parsers.inner(pos), Isar_Token.reader(tokens, start)) match {
+ case Parsers.Success(res, _) => Some(res)
+ case _ => None
+ }
+ }
+
+ def errors: List[String] =
+ if (parse.isDefined) Nil
+ else List("Malformed citation" + Position.here(pos))
+
+ override def toString: String =
+ parse match {
+ case Some(inner) => inner.toString
+ case None => "<malformed>"
+ }
+ }
+
+ object Parsers extends Parse.Parsers {
+ val keywords: Keyword.Keywords = Thy_Header.bootstrap_keywords + "in" + "using"
+
+ val location: Parser[String] = embedded ~ $$$("in") ^^ { case x ~ _ => x } | success("")
+ val citations: Parser[String] = rep1sep(name, $$$("and")) ^^ (x => x.mkString(","))
+ val kind: Parser[String] = $$$("using") ~! name ^^ { case _ ~ x => x } | success(CITE)
+
+ def inner(pos: Position.T): Parser[Inner] =
+ location ~ citations ~ kind ^^
+ { case x ~ y ~ z => Inner(z, y, XML.string(x), pos) }
+ }
+
+ def parse(
+ cite_commands: List[String],
+ text: String,
+ start: Isar_Token.Pos = Isar_Token.Pos.start
+ ): List[Outer] = {
+ val controls = cite_commands.map(s => Symbol.control_prefix + s + Symbol.control_suffix)
+ val special = (controls ::: controls.map(Symbol.decode)).toSet
+
+ val Parsers = Antiquote.Parsers
+ Parsers.parseAll(Parsers.rep(Parsers.antiquote_special(special)), text) match {
+ case Parsers.Success(ants, _) =>
+ var pos = start
+ val result = new mutable.ListBuffer[Outer]
+ for (ant <- ants) {
+ ant match {
+ case Antiquote.Control(source) =>
+ for {
+ head <- Symbol.iterator(source).nextOption
+ kind <- Symbol.control_name(Symbol.encode(head))
+ } {
+ val rest = source.substring(head.length)
+ val (body, pos1) =
+ if (rest.isEmpty) (rest, pos)
+ else (Scan.Parsers.cartouche_content(rest), pos.advance(Symbol.open))
+ result += Outer(kind, body, pos1)
+ }
+ case _ =>
+ }
+ pos = pos.advance(ant.source)
+ }
+ result.toList
+ case _ => error("Unexpected failure parsing special antiquotations:\n" + text)
+ }
+ }
+ }
+
+
+ /* update old forms: @{cite ...} and \cite{...} */
+
+ def cite_antiquotation(name: String, body: String): String =
+ """\<^""" + name + """>\<open>""" + body + """\<close>"""
+
+ def cite_antiquotation(name: String, location: String, citations: List[String]): String = {
+ val body =
+ if_proper(location, Symbol.cartouche(location) + " in ") +
+ citations.map(quote).mkString(" and ")
+ cite_antiquotation(name, body)
+ }
+
+ private val Cite_Command = """\\(cite|nocite|citet|citep)((?:\[[^\]]*\])?)\{([^}]*)\}""".r
+ private val Cite_Macro = """\[\s*cite_macro\s*=\s*"?(\w+)"?\]\s*""".r
+
+ def update_cite_commands(str: String): String =
+ Cite_Command.replaceAllIn(str, { m =>
+ val name = m.group(1)
+ val loc = m.group(2)
+ val location =
+ if (loc.startsWith("[") && loc.endsWith("]")) loc.substring(1, loc.length - 1)
+ else loc
+ val citations = space_explode(',', m.group(3)).map(_.trim)
+ Regex.quoteReplacement(cite_antiquotation(name, location, citations))
+ })
+
+ def update_cite_antiquotation(cite_commands: List[String], str: String): String = {
+ val opt_body =
+ for {
+ str1 <- Library.try_unprefix("@{cite", str)
+ str2 <- Library.try_unsuffix("}", str1)
+ } yield str2.trim
+
+ opt_body match {
+ case None => str
+ case Some(body0) =>
+ val (name, body1) =
+ Cite_Macro.findFirstMatchIn(body0) match {
+ case None => (CITE, body0)
+ case Some(m) => (m.group(1), Cite_Macro.replaceAllIn(body0, ""))
+ }
+ val body2 = body1.replace("""\<close>""", """\<close> in""")
+ if (cite_commands.contains(name)) cite_antiquotation(name, body2)
+ else cite_antiquotation(CITE, body2 + " using " + quote(name))
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/latex.ML Sat Jan 20 16:09:35 2024 +0100
@@ -0,0 +1,262 @@
+(* Title: Pure/General/latex.ML
+ Author: Makarius
+
+Support for LaTeX.
+*)
+
+signature LATEX =
+sig
+ type text = XML.body
+ val text: string * Position.T -> text
+ val string: string -> text
+ val block: text -> XML.tree
+ val output: text -> text
+ val macro0: string -> text
+ val macro: string -> text -> text
+ val environment: string -> text -> text
+ val output_name: string -> string
+ val output_ascii: string -> string
+ val output_ascii_breakable: string -> string -> string
+ val output_symbols: Symbol.symbol list -> string
+ val output_syms: string -> string
+ val symbols: Symbol_Pos.T list -> text
+ val symbols_output: Symbol_Pos.T list -> text
+ val isabelle_body: string -> text -> text
+ val theory_entry: string -> string
+ val cite: {kind: string, citations: (string * Position.T) list, location: text} -> text
+ type index_item = {text: text, like: string}
+ type index_entry = {items: index_item list, def: bool}
+ val index_entry: index_entry -> text
+ val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a
+ val latexN: string
+ val latex_markup: string * Properties.T -> Markup.output
+end;
+
+structure Latex: LATEX =
+struct
+
+(* text with positions *)
+
+type text = XML.body;
+
+fun text (s, pos) =
+ if s = "" then []
+ else if pos = Position.none then [XML.Text s]
+ else [XML.Elem (Position.markup pos Markup.document_latex, [XML.Text s])];
+
+fun string s = text (s, Position.none);
+
+fun block body = XML.Elem (Markup.document_latex, body);
+
+fun output body = [XML.Elem (Markup.latex_output, body)];
+
+fun macro0 name = [XML.Elem (Markup.latex_macro0 name, [])];
+fun macro name body = [XML.Elem (Markup.latex_macro name, body)];
+fun environment name body = [XML.Elem (Markup.latex_environment name, body)];
+
+
+(* output name for LaTeX macros *)
+
+val output_name =
+ translate_string
+ (fn "_" => "UNDERSCORE"
+ | "'" => "PRIME"
+ | "0" => "ZERO"
+ | "1" => "ONE"
+ | "2" => "TWO"
+ | "3" => "THREE"
+ | "4" => "FOUR"
+ | "5" => "FIVE"
+ | "6" => "SIX"
+ | "7" => "SEVEN"
+ | "8" => "EIGHT"
+ | "9" => "NINE"
+ | s => s);
+
+fun enclose_name bg en = enclose bg en o output_name;
+
+
+(* output verbatim ASCII *)
+
+val output_ascii =
+ translate_string
+ (fn " " => "\\ "
+ | "\t" => "\\ "
+ | "\n" => "\\isanewline\n"
+ | s =>
+ s
+ |> member_string "\"#$%&',-<>\\^_`{}~" s ? enclose "{\\char`\\" "}"
+ |> suffix "{\\kern0pt}");
+
+fun output_ascii_breakable sep =
+ space_explode sep
+ #> map output_ascii
+ #> space_implode (output_ascii sep ^ "\\discretionary{}{}{}");
+
+
+(* output symbols *)
+
+local
+
+val char_table =
+ Symtab.make
+ [("\007", "{\\isacharbell}"),
+ ("!", "{\\isacharbang}"),
+ ("\"", "{\\isachardoublequote}"),
+ ("#", "{\\isacharhash}"),
+ ("$", "{\\isachardollar}"),
+ ("%", "{\\isacharpercent}"),
+ ("&", "{\\isacharampersand}"),
+ ("'", "{\\isacharprime}"),
+ ("(", "{\\isacharparenleft}"),
+ (")", "{\\isacharparenright}"),
+ ("*", "{\\isacharasterisk}"),
+ ("+", "{\\isacharplus}"),
+ (",", "{\\isacharcomma}"),
+ ("-", "{\\isacharminus}"),
+ (".", "{\\isachardot}"),
+ ("/", "{\\isacharslash}"),
+ (":", "{\\isacharcolon}"),
+ (";", "{\\isacharsemicolon}"),
+ ("<", "{\\isacharless}"),
+ ("=", "{\\isacharequal}"),
+ (">", "{\\isachargreater}"),
+ ("?", "{\\isacharquery}"),
+ ("@", "{\\isacharat}"),
+ ("[", "{\\isacharbrackleft}"),
+ ("\\", "{\\isacharbackslash}"),
+ ("]", "{\\isacharbrackright}"),
+ ("^", "{\\isacharcircum}"),
+ ("_", "{\\isacharunderscore}"),
+ ("`", "{\\isacharbackquote}"),
+ ("{", "{\\isacharbraceleft}"),
+ ("|", "{\\isacharbar}"),
+ ("}", "{\\isacharbraceright}"),
+ ("~", "{\\isachartilde}")];
+
+fun output_chr " " = "\\ "
+ | output_chr "\t" = "\\ "
+ | output_chr "\n" = "\\isanewline\n"
+ | output_chr c =
+ (case Symtab.lookup char_table c of
+ SOME s => s ^ "{\\kern0pt}"
+ | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
+
+fun output_sym sym =
+ (case Symbol.decode sym of
+ Symbol.Char s => output_chr s
+ | Symbol.UTF8 s => s
+ | Symbol.Sym s => enclose_name "{\\isasym" "}" s
+ | Symbol.Control s => enclose_name "\\isactrl" " " s
+ | Symbol.Malformed s => error (Symbol.malformed_msg s)
+ | Symbol.EOF => error "Bad EOF symbol");
+
+open Basic_Symbol_Pos;
+
+val scan_latex_length =
+ Scan.many1 (fn (s, _) => s <> Symbol.latex andalso Symbol.not_eof s)
+ >> (Symbol.length o map Symbol_Pos.symbol) ||
+ $$ Symbol.latex -- Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0;
+
+val scan_latex =
+ $$ Symbol.latex |-- Symbol_Pos.scan_cartouche_content "Embedded LaTeX: "
+ >> (implode o map Symbol_Pos.symbol) ||
+ Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_sym o Symbol_Pos.symbol);
+
+fun read scan syms =
+ Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms);
+
+in
+
+val length_symbols =
+ Integer.build o fold Integer.add o these o read scan_latex_length;
+
+fun output_symbols syms =
+ if member (op =) syms Symbol.latex then
+ (case read scan_latex syms of
+ SOME ss => implode ss
+ | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
+ else implode (map output_sym syms);
+
+val output_syms = output_symbols o Symbol.explode;
+
+end;
+
+fun symbols syms = text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms));
+fun symbols_output syms =
+ text (output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms));
+
+
+(* theory presentation *)
+
+fun isabelle_body name =
+ XML.enclose
+ ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n")
+ "%\n\\end{isabellebody}%\n";
+
+fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
+
+
+(* cite: references to bibliography *)
+
+fun cite {kind, location, citations} =
+ let
+ val _ =
+ citations |> List.app (fn (s, pos) =>
+ if member_string s ","
+ then error ("Single citation expected, without commas" ^ Position.here pos)
+ else ());
+ val citations' = space_implode "," (map #1 citations);
+ val markup = Markup.latex_cite {kind = kind, citations = citations'};
+ in [XML.Elem (markup, location)] end;
+
+
+(* index entries *)
+
+type index_item = {text: text, like: string};
+type index_entry = {items: index_item list, def: bool};
+
+fun index_item (item: index_item) =
+ XML.wrap_elem ((Markup.latex_index_item, #text item), XML.string (#like item));
+
+fun index_entry (entry: index_entry) =
+ [XML.Elem (Markup.latex_index_entry (if #def entry then "isaindexdef" else "isaindexref"),
+ map index_item (#items entry))];
+
+fun index_binding NONE = I
+ | index_binding (SOME def) = Binding.map_name (suffix (if def then "_def" else "_ref"));
+
+fun index_variants setup binding =
+ fold (fn index => setup (index_binding index binding) index) [NONE, SOME true, SOME false];
+
+
+(* print mode *)
+
+val latexN = "latex";
+
+local
+
+fun latex_output str =
+ let val syms = Symbol.explode str
+ in (output_symbols syms, length_symbols syms) end;
+
+val command_markup = YXML.output_markup (Markup.latex_macro "isacommand");
+val keyword_markup = YXML.output_markup (Markup.latex_macro "isakeyword");
+val indent_markup = YXML.output_markup (Markup.latex_macro "isaindent");
+
+in
+
+fun latex_markup (s, _: Properties.T) =
+ if member (op =) [Markup.commandN, Markup.keyword1N, Markup.keyword3N] s then command_markup
+ else if s = Markup.keyword2N then keyword_markup
+ else Markup.no_output;
+
+val _ = Output.add_mode latexN latex_output (prefix Symbol.latex o cartouche);
+val _ = Markup.add_mode latexN latex_markup;
+
+val _ = Pretty.add_mode latexN
+ (fn s => fn _ => if s = "" then s else uncurry enclose indent_markup s);
+
+end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/latex.scala Sat Jan 20 16:09:35 2024 +0100
@@ -0,0 +1,469 @@
+/* Title: Pure/General/latex.scala
+ Author: Makarius
+
+Support for LaTeX.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+
+import scala.annotation.tailrec
+import scala.collection.mutable
+import scala.collection.immutable.TreeMap
+import scala.util.matching.Regex
+
+
+object Latex {
+ /* output name for LaTeX macros */
+
+ private val output_name_map: Map[Char, String] =
+ Map('_' -> "UNDERSCORE",
+ '\'' -> "PRIME",
+ '0' -> "ZERO",
+ '1' -> "ONE",
+ '2' -> "TWO",
+ '3' -> "THREE",
+ '4' -> "FOUR",
+ '5' -> "FIVE",
+ '6' -> "SIX",
+ '7' -> "SEVEN",
+ '8' -> "EIGHT",
+ '9' -> "NINE")
+
+ def output_name(name: String): String =
+ if (name.exists(output_name_map.keySet)) {
+ val res = new StringBuilder
+ for (c <- name) {
+ output_name_map.get(c) match {
+ case None => res += c
+ case Some(s) => res ++= s
+ }
+ }
+ res.toString
+ }
+ else name
+
+
+ /* index entries */
+
+ def index_escape(str: String): String = {
+ val special1 = "!\"@|"
+ val special2 = "\\{}#"
+ if (str.exists(c => special1.contains(c) || special2.contains(c))) {
+ val res = new StringBuilder
+ for (c <- str) {
+ if (special1.contains(c)) {
+ res ++= "\\char"
+ res ++= Value.Int(c)
+ }
+ else {
+ if (special2.contains(c)) { res += '"'}
+ res += c
+ }
+ }
+ res.toString
+ }
+ else str
+ }
+
+ object Index_Item {
+ sealed case class Value(text: Text, like: String)
+ def unapply(tree: XML.Tree): Option[Value] =
+ tree match {
+ case XML.Wrapped_Elem(Markup.Latex_Index_Item(_), text, like) =>
+ Some(Value(text, XML.content(like)))
+ case _ => None
+ }
+ }
+
+ object Index_Entry {
+ sealed case class Value(items: List[Index_Item.Value], kind: String)
+ def unapply(tree: XML.Tree): Option[Value] =
+ tree match {
+ case XML.Elem(Markup.Latex_Index_Entry(kind), body) =>
+ val items = body.map(Index_Item.unapply)
+ if (items.forall(_.isDefined)) Some(Value(items.map(_.get), kind)) else None
+ case _ => None
+ }
+ }
+
+
+ /* tags */
+
+ object Tags {
+ enum Op { case fold, drop, keep }
+
+ val standard = "document,theory,proof,ML,visible,-invisible,important,unimportant"
+
+ private def explode(spec: String): List[String] = space_explode(',', spec)
+
+ def apply(spec: String): Tags =
+ new Tags(spec,
+ (explode(standard) ::: explode(spec)).foldLeft(TreeMap.empty[String, Op]) {
+ case (m, tag) =>
+ tag.toList match {
+ case '/' :: cs => m + (cs.mkString -> Op.fold)
+ case '-' :: cs => m + (cs.mkString -> Op.drop)
+ case '+' :: cs => m + (cs.mkString -> Op.keep)
+ case cs => m + (cs.mkString -> Op.keep)
+ }
+ })
+
+ val empty: Tags = apply("")
+ }
+
+ class Tags private(spec: String, map: TreeMap[String, Tags.Op]) {
+ override def toString: String = spec
+
+ def get(name: String): Option[Tags.Op] = map.get(name)
+
+ def sty(comment_latex: Boolean): File.Content = {
+ val path = Path.explode("isabelletags.sty")
+ val comment =
+ if (comment_latex) """\usepackage{comment}"""
+ else """%plain TeX version of comment package -- much faster!
+\let\isafmtname\fmtname\def\fmtname{plain}
+\usepackage{comment}
+\let\fmtname\isafmtname"""
+ val tags =
+ (for ((name, op) <- map.iterator)
+ yield "\\isa" + op + "tag{" + name + "}").toList
+ File.content(path, comment + """
+
+\newcommand{\isakeeptag}[1]%
+{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
+\newcommand{\isadroptag}[1]%
+{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
+\newcommand{\isafoldtag}[1]%
+{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
+
+""" + terminate_lines(tags))
+ }
+ }
+
+
+ /* output text and positions */
+
+ type Text = XML.Body
+
+ def position(a: String, b: String): String = "%:%" + a + "=" + b + "%:%\n"
+
+ def init_position(file_pos: String): List[String] =
+ if (file_pos.isEmpty) Nil
+ else List("\\endinput\n", position(Markup.FILE, file_pos))
+
+ def append_position(path: Path, file_pos: String): Unit = {
+ val pos = init_position(file_pos).mkString
+ if (pos.nonEmpty) {
+ val sep = if (File.read(path).endsWith("\n")) "" else "\n"
+ File.append(path, sep + pos)
+ }
+ }
+
+ def copy_file(src: Path, dst: Path): Unit = {
+ Isabelle_System.copy_file(src, dst)
+ if (src.is_latex) {
+ val target = if (dst.is_dir) dst + src.base else dst
+ val file_pos = File.symbolic_path(src)
+ append_position(target, file_pos)
+ }
+ }
+
+ def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = {
+ Isabelle_System.copy_file_base(base_dir, src, target_dir)
+ if (src.is_latex) {
+ val file_pos = File.symbolic_path(base_dir + src)
+ append_position(target_dir + src, file_pos)
+ }
+ }
+
+ class Output(val options: Options) {
+ def latex_output(latex_text: Text): String = make(latex_text)
+
+ def latex_macro0(name: String, optional_argument: String = ""): Text =
+ XML.string("\\" + name + optional_argument)
+
+ def latex_macro(name: String, body: Text, optional_argument: String = ""): Text =
+ XML.enclose("\\" + name + optional_argument + "{", "}", body)
+
+ def latex_environment(name: String, body: Text, optional_argument: String = ""): Text =
+ XML.enclose(
+ "%\n\\begin{" + name + "}" + optional_argument + "%\n",
+ "%\n\\end{" + name + "}", body)
+
+ def latex_heading(kind: String, body: Text, optional_argument: String = ""): Text =
+ XML.enclose(
+ "%\n\\" + options.string("document_heading_prefix") + kind + optional_argument + "{",
+ "%\n}\n", body)
+
+ def latex_body(kind: String, body: Text, optional_argument: String = ""): Text =
+ latex_environment("isamarkup" + kind, body, optional_argument)
+
+ def latex_tag(name: String, body: Text, delim: Boolean = false): Text = {
+ val s = output_name(name)
+ val kind = if (delim) "delim" else "tag"
+ val end = if (delim) "" else "{\\isafold" + s + "}%\n"
+ if (options.bool("document_comment_latex")) {
+ XML.enclose(
+ "%\n\\begin{isa" + kind + s + "}\n",
+ "%\n\\end{isa" + kind + s + "}\n" + end, body)
+ }
+ else {
+ XML.enclose(
+ "%\n\\isa" + kind + s + "\n",
+ "%\n\\endisa" + kind + s + "\n" + end, body)
+ }
+ }
+
+ def cite(inner: Bibtex.Cite.Inner): Text = {
+ val body =
+ latex_macro0(inner.kind) :::
+ (if (inner.location.isEmpty) Nil
+ else XML.string("[") ::: inner.location ::: XML.string("]")) :::
+ XML.string("{" + inner.citations + "}")
+
+ if (inner.pos.isEmpty) body
+ else List(XML.Elem(Markup.Latex_Output(inner.pos), body))
+ }
+
+ def index_item(item: Index_Item.Value): String = {
+ val like = if_proper(item.like, index_escape(item.like) + "@")
+ val text = index_escape(latex_output(item.text))
+ like + text
+ }
+
+ def index_entry(entry: Index_Entry.Value): Text = {
+ val items = entry.items.map(index_item).mkString("!")
+ val kind = if_proper(entry.kind, "|" + index_escape(entry.kind))
+ latex_macro("index", XML.string(items + kind))
+ }
+
+
+ /* standard output of text with per-line positions */
+
+ def unknown_elem(elem: XML.Elem, pos: Position.T): XML.Body =
+ error("Unknown latex markup element " + quote(elem.name) + Position.here(pos) +
+ ":\n" + XML.string_of_tree(elem))
+
+ def make(
+ latex_text: Text,
+ file_pos: String = "",
+ line_pos: Properties.T => Option[Int] = Position.Line.unapply
+ ): String = {
+ var line = 1
+ val result = new mutable.ListBuffer[String]
+ val positions = new mutable.ListBuffer[String] ++= init_position(file_pos)
+
+ val file_position = if (file_pos.isEmpty) Position.none else Position.File(file_pos)
+
+ def traverse(xml: XML.Body): Unit = {
+ xml.foreach {
+ case XML.Text(s) =>
+ line += Library.count_newlines(s)
+ result += s
+ case elem @ XML.Elem(markup, body) =>
+ val a = Markup.Optional_Argument.get(markup.properties)
+ traverse {
+ markup match {
+ case Markup.Document_Latex(props) =>
+ if (positions.nonEmpty) {
+ for (l <- line_pos(props)) {
+ val s = position(Value.Int(line), Value.Int(l))
+ if (positions.last != s) positions += s
+ }
+ }
+ body
+ case Markup.Latex_Output(_) => XML.string(latex_output(body))
+ case Markup.Latex_Macro0(name) if body.isEmpty => latex_macro0(name, a)
+ case Markup.Latex_Macro(name) => latex_macro(name, body, a)
+ case Markup.Latex_Environment(name) => latex_environment(name, body, a)
+ case Markup.Latex_Heading(kind) => latex_heading(kind, body, a)
+ case Markup.Latex_Body(kind) => latex_body(kind, body, a)
+ case Markup.Latex_Delim(name) => latex_tag(name, body, delim = true)
+ case Markup.Latex_Tag(name) => latex_tag(name, body)
+ case Markup.Latex_Cite(_) =>
+ elem match {
+ case Bibtex.Cite(inner) => cite(inner)
+ case _ => unknown_elem(elem, file_position)
+ }
+ case Markup.Latex_Index_Entry(_) =>
+ elem match {
+ case Index_Entry(entry) => index_entry(entry)
+ case _ => unknown_elem(elem, file_position)
+ }
+ case _ => unknown_elem(elem, file_position)
+ }
+ }
+ }
+ }
+ traverse(latex_text)
+
+ result ++= positions
+ result.mkString
+ }
+ }
+
+
+ /* generated .tex file */
+
+ private val File_Pattern = """^%:%file=(.+)%:%$""".r
+ private val Line_Pattern = """^*%:%(\d+)=(\d+)%:%$""".r
+
+ def read_tex_file(tex_file: Path): Tex_File = {
+ val positions =
+ Line.logical_lines(File.read(tex_file)).reverse.
+ takeWhile(_ != "\\endinput").reverse
+
+ val source_file =
+ positions match {
+ case File_Pattern(file) :: _ => Some(file)
+ case _ => None
+ }
+
+ val source_lines =
+ if (source_file.isEmpty) Nil
+ else
+ positions.flatMap(line =>
+ line match {
+ case Line_Pattern(Value.Int(line), Value.Int(source_line)) => Some(line -> source_line)
+ case _ => None
+ })
+
+ new Tex_File(tex_file, source_file, source_lines)
+ }
+
+ final class Tex_File private[Latex](
+ tex_file: Path,
+ source_file: Option[String],
+ source_lines: List[(Int, Int)]
+ ) {
+ override def toString: String = tex_file.toString
+
+ def source_position(l: Int): Option[Position.T] =
+ source_file match {
+ case None => None
+ case Some(file) =>
+ val source_line =
+ source_lines.iterator.takeWhile({ case (m, _) => m <= l }).
+ foldLeft(0) { case (_, (_, n)) => n }
+ if (source_line == 0) None else Some(Position.Line_File(source_line, file))
+ }
+
+ def position(line: Int): Position.T =
+ source_position(line) getOrElse
+ Position.Line_File(line, source_file.getOrElse(tex_file.implode))
+ }
+
+
+ /* latex log */
+
+ def latex_errors(dir: Path, root_name: String): List[String] = {
+ val root_log_path = dir + Path.explode(root_name).log
+ if (root_log_path.is_file) {
+ for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
+ yield "Latex error" + Position.here(pos) + ":\n" + Library.indent_lines(2, msg)
+ }
+ else Nil
+ }
+
+ def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] = {
+ val seen_files = Synchronized(Map.empty[JFile, Tex_File])
+
+ def check_tex_file(path: Path): Option[Tex_File] =
+ seen_files.change_result(seen =>
+ seen.get(path.file) match {
+ case None =>
+ if (path.is_file) {
+ val tex_file = read_tex_file(path)
+ (Some(tex_file), seen + (path.file -> tex_file))
+ }
+ else (None, seen)
+ case some => (some, seen)
+ })
+
+ def tex_file_position(path: Path, line: Int): Position.T =
+ check_tex_file(path) match {
+ case Some(tex_file) => tex_file.position(line)
+ case None => Position.Line_File(line, path.implode)
+ }
+
+ object File_Line_Error {
+ val Pattern: Regex = """^(.*?\.\w\w\w):(\d+): (.*)$""".r
+ def unapply(line: String): Option[(Path, Int, String)] =
+ line match {
+ case Pattern(file, Value.Int(line), message) =>
+ val path = File.standard_path(file)
+ if (Path.is_wellformed(path)) {
+ val file = (dir + Path.explode(path)).canonical
+ val msg = Library.perhaps_unprefix("LaTeX Error: ", message)
+ if (file.is_file) Some((file, line, msg)) else None
+ }
+ else None
+ case _ => None
+ }
+ }
+
+ val Line_Error = """^l\.\d+ (.*)$""".r
+ val More_Error =
+ List(
+ "<argument>",
+ "<template>",
+ "<recently read>",
+ "<to be read again>",
+ "<inserted text>",
+ "<output>",
+ "<everypar>",
+ "<everymath>",
+ "<everydisplay>",
+ "<everyhbox>",
+ "<everyvbox>",
+ "<everyjob>",
+ "<everycr>",
+ "<mark>",
+ "<everyeof>",
+ "<write>").mkString("^(?:", "|", ") (.*)$").r
+
+ val Bad_Font = """^LaTeX Font Warning: (Font .*\btxmia\b.* undefined).*$""".r
+ val Bad_File = """^! LaTeX Error: (File `.*' not found\.)$""".r
+
+ val error_ignore =
+ Set(
+ "See the LaTeX manual or LaTeX Companion for explanation.",
+ "Type H <return> for immediate help.")
+
+ def error_suffix1(lines: List[String]): Option[String] = {
+ val lines1 =
+ lines.take(20).takeWhile({ case File_Line_Error((_, _, _)) => false case _ => true })
+ lines1.zipWithIndex.collectFirst({
+ case (Line_Error(msg), i) =>
+ cat_lines(lines1.take(i).filterNot(error_ignore) ::: List(msg)) })
+ }
+ def error_suffix2(lines: List[String]): Option[String] =
+ lines match {
+ case More_Error(msg) :: _ => Some(msg)
+ case _ => None
+ }
+
+ @tailrec def filter(
+ lines: List[String],
+ result: List[(String, Position.T)]
+ ) : List[(String, Position.T)] = {
+ lines match {
+ case File_Line_Error((file, line, msg1)) :: rest1 =>
+ val pos = tex_file_position(file, line)
+ val msg2 = error_suffix1(rest1) orElse error_suffix2(rest1) getOrElse ""
+ filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result)
+ case Bad_Font(msg) :: rest =>
+ filter(rest, (msg, Position.none) :: result)
+ case Bad_File(msg) :: rest =>
+ filter(rest, (msg, Position.none) :: result)
+ case _ :: rest => filter(rest, result)
+ case Nil => result.reverse
+ }
+ }
+
+ filter(Line.logical_lines(root_log), Nil)
+ }
+}
--- a/src/Pure/ROOT.ML Sat Jan 20 15:07:41 2024 +0100
+++ b/src/Pure/ROOT.ML Sat Jan 20 16:09:35 2024 +0100
@@ -241,7 +241,7 @@
ML_file "PIDE/command_span.ML";
ML_file "Thy/thy_element.ML";
ML_file "Thy/markdown.ML";
-ML_file "Thy/latex.ML";
+ML_file "General/latex.ML";
(*ML with context and antiquotations*)
ML_file "ML/ml_context.ML";
@@ -345,7 +345,7 @@
ML_file "System/isabelle_process.ML";
ML_file "System/scala_compiler.ML";
ML_file "System/isabelle_tool.ML";
-ML_file "Thy/bibtex.ML";
+ML_file "General/bibtex.ML";
ML_file "PIDE/protocol.ML";
ML_file "General/output_primitives_virtual.ML";
--- a/src/Pure/Thy/bibtex.ML Sat Jan 20 15:07:41 2024 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,134 +0,0 @@
-(* Title: Pure/Thy/bibtex.ML
- Author: Makarius
-
-BibTeX support.
-*)
-
-signature BIBTEX =
-sig
- val check_database:
- Position.T -> string -> (string * Position.T) list * (string * Position.T) list
- val check_database_output: Position.T -> string -> unit
- val check_bibtex_entry: Proof.context -> string * Position.T -> unit
- val cite_macro: string Config.T
- val cite_antiquotation: binding -> (Proof.context -> string) -> theory -> theory
-end;
-
-structure Bibtex: BIBTEX =
-struct
-
-(* check database *)
-
-type message = string * Position.T;
-
-fun check_database pos0 database =
- \<^scala>\<open>bibtex_check_database\<close> database
- |> YXML.parse_body
- |> 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.properties_of pos0));
-
-fun check_database_output pos0 database =
- 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) =>
- warning ("Bibtex warning" ^ Position.here pos ^ ":\n " ^ msg))
- end;
-
-
-(* check bibtex entry *)
-
-fun check_bibtex_entry ctxt (name, pos) =
- let
- fun warn () =
- if Context_Position.is_visible ctxt then
- 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 = Properties.get_string props Markup.nameN;
- val pos = Position.of_properties props;
- in (name, pos) end;
- in
- if name = "*" then ()
- else
- (case Position.id_of pos of
- NONE => warn ()
- | SOME id =>
- (case \<^scala>\<open>bibtex_session_entries\<close> [id] of
- [] => warn ()
- | _ :: entries =>
- Completion.check_entity Markup.bibtex_entryN (map decode entries)
- ctxt (name, pos) |> ignore))
- end;
-
-
-(* document antiquotations *)
-
-val cite_macro = Attrib.setup_config_string \<^binding>\<open>cite_macro\<close> (K "");
-fun get_cite_macro ctxt = Config.get ctxt cite_macro;
-
-val _ =
- Theory.setup (Document_Antiquotation.setup_option \<^binding>\<open>cite_macro\<close> (Config.put cite_macro));
-
-
-local
-
-val parse_citations = Parse.and_list1 (Parse.position Parse.name);
-
-fun cite_command ctxt get_kind ((opt_loc, citations), macro_name) =
- let
- val loc = the_default Input.empty opt_loc;
- val _ = Context_Position.reports ctxt (Document_Output.document_reports loc);
- val _ = List.app (check_bibtex_entry ctxt) citations;
-
- val kind = if macro_name = "" then get_kind ctxt else macro_name;
- val location = Document_Output.output_document ctxt {markdown = false} loc;
- in Latex.cite {kind = kind, citations = citations, location = location} end;
-
-fun cite_command_old ctxt get_kind args =
- let
- val _ =
- if Context_Position.is_visible ctxt then
- legacy_feature ("Old antiquotation syntax, better use \"isabelle update -u cite\"" ^
- Position.here_list (map snd (snd args)))
- else ();
- in cite_command ctxt get_kind (args, "") end;
-
-val cite_keywords =
- Thy_Header.bootstrap_keywords
- |> Keyword.add_keywords (map (fn a => ((a, Position.none), Keyword.no_spec)) ["in", "using"]);
-
-fun cite_command_embedded ctxt get_kind input =
- let
- val parser =
- Scan.option (Parse.embedded_input --| Parse.$$$ "in") -- parse_citations --
- Scan.optional (Parse.$$$ "using" |-- Parse.!!! Parse.name) "";
- val args = Parse.read_embedded ctxt cite_keywords parser input;
- in cite_command ctxt get_kind args end;
-
-fun cite_command_parser get_kind =
- Scan.option Args.cartouche_input -- parse_citations
- >> (fn args => fn ctxt => cite_command_old ctxt get_kind args) ||
- Parse.embedded_input
- >> (fn arg => fn ctxt => cite_command_embedded ctxt get_kind arg);
-
-in
-
-fun cite_antiquotation binding get_kind =
- Document_Output.antiquotation_raw binding (Scan.lift (cite_command_parser get_kind))
- (fn ctxt => fn cmd => cmd ctxt);
-
-end;
-
-val _ =
- Theory.setup
- (cite_antiquotation \<^binding>\<open>cite\<close> get_cite_macro #>
- cite_antiquotation \<^binding>\<open>nocite\<close> (K "nocite") #>
- cite_antiquotation \<^binding>\<open>citet\<close> (K "citet") #>
- cite_antiquotation \<^binding>\<open>citep\<close> (K "citep"));
-
-end;
--- a/src/Pure/Thy/bibtex.scala Sat Jan 20 15:07:41 2024 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,855 +0,0 @@
-/* Title: Pure/Thy/bibtex.scala
- Author: Makarius
-
-BibTeX support.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile}
-
-import scala.collection.mutable
-import scala.util.parsing.combinator.RegexParsers
-import scala.util.parsing.input.Reader
-import scala.util.matching.Regex
-
-import isabelle.{Token => Isar_Token}
-
-
-object Bibtex {
- /** file format **/
-
- class File_Format extends isabelle.File_Format {
- val format_name: String = "bibtex"
- val file_ext: String = "bib"
-
- override def parse_data(name: String, text: String): Bibtex.Entries =
- Bibtex.Entries.parse(text, Isar_Token.Pos.file(name))
-
- override def theory_suffix: String = "bibtex_file"
- override def theory_content(name: String): String =
- """theory "bib" imports Pure begin bibtex_file "." end"""
- override def theory_excluded(name: String): Boolean = name == "bib"
-
- override def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = {
- val name = snapshot.node_name
- if (detect(name.node)) {
- val title = "Bibliography " + quote(snapshot.node_name.file_name)
- val content =
- Isabelle_System.with_tmp_file("bib", "bib") { bib =>
- File.write(bib, snapshot.node.source)
- Bibtex.html_output(List(bib), style = "unsort", title = title)
- }
- Some(Browser_Info.HTML_Document(title, content))
- }
- else None
- }
- }
-
-
-
- /** bibtex errors **/
-
- def bibtex_errors(dir: Path, root_name: String): List[String] = {
- val log_path = dir + Path.explode(root_name).blg
- if (log_path.is_file) {
- val Error1 = """^(I couldn't open database file .+)$""".r
- val Error2 = """^(I found no .+)$""".r
- val Error3 = """^(.+)---line (\d+) of file (.+)""".r
- Line.logical_lines(File.read(log_path)).flatMap(line =>
- line match {
- case Error1(msg) => Some("Bibtex error: " + msg)
- case Error2(msg) => Some("Bibtex error: " + msg)
- case Error3(msg, Value.Int(l), file) =>
- val path = File.standard_path(file)
- if (Path.is_wellformed(path)) {
- val pos = Position.Line_File(l, (dir + Path.explode(path)).canonical.implode)
- Some("Bibtex error" + Position.here(pos) + ":\n " + msg)
- }
- else None
- case _ => None
- })
- }
- else Nil
- }
-
-
-
- /** check database **/
-
- 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]
- val tokens = new mutable.ListBuffer[(Token, Position.T)]
- var line = 1
- var offset = 1
-
- def make_pos(length: Int): Position.T =
- Position.Offset(offset) ::: Position.End_Offset(offset + length) ::: Position.Line(line)
-
- def advance_pos(tok: Token): Unit = {
- for (s <- Symbol.iterator(tok.source)) {
- if (Symbol.is_newline(s)) line += 1
- offset += 1
- }
- }
-
- def get_line_pos(l: Int): Position.T =
- if (0 < l && l <= tokens.length) tokens(l - 1)._2 else Position.none
-
- for (chunk <- chunks) {
- val name = chunk.name
- if (name != "" && !chunk_pos.isDefinedAt(name)) {
- chunk_pos += (name -> make_pos(chunk.heading_length))
- }
- for (tok <- chunk.tokens) {
- tokens += (tok.copy(source = tok.source.replace("\n", " ")) -> make_pos(tok.source.length))
- advance_pos(tok)
- }
- }
-
- Isabelle_System.with_tmp_dir("bibtex") { tmp_dir =>
- File.write(tmp_dir + Path.explode("root.bib"),
- tokens.iterator.map(p => p._1.source).mkString("", "\n", "\n"))
- File.write(tmp_dir + Path.explode("root.aux"),
- "\\bibstyle{plain}\n\\bibdata{root}\n\\citation{*}")
- Isabelle_System.bash("\"$ISABELLE_BIBTEX\" root", cwd = tmp_dir.file)
-
- val Error = """^(.*)---line (\d+) of file root.bib$""".r
- val Warning = """^Warning--(.+)$""".r
- val Warning_Line = """--line (\d+) of file root.bib$""".r
- val Warning_in_Chunk = """^Warning--(.+) in (.+)$""".r
-
- 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
-
- val (errors, warnings) =
- if (lines.isEmpty) (Nil, Nil)
- else {
- 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.capitalized(msg) + " in entry " + quote(name), chunk_pos(name))))
- case (Warning(msg), Warning_Line(Value.Int(l))) =>
- Some((false, (Word.capitalized(msg), get_line_pos(l))))
- case (Warning(msg), _) =>
- Some((false, (Word.capitalized(msg), Position.none)))
- case _ => None
- }
- ).partition(_._1)
- }
- (errors.map(_._2), warnings.map(_._2))
- }
- }
-
- object Check_Database extends Scala.Fun_String("bibtex_check_database") {
- val here = Scala_Project.here
- def apply(database: String): String = {
- import XML.Encode._
- YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))(
- check_database(database)))
- }
- }
-
-
-
- /** document model **/
-
- /* entries */
-
- sealed case class Entry(name: String, pos: Position.T) {
- def encode: String = YXML.string_of_body(XML.Encode.properties(Markup.Name(name) ::: pos))
- }
-
- object Entries {
- val empty: Entries = apply(Nil)
-
- def apply(entries: List[Entry], errors: List[String] = Nil): Entries =
- new Entries(entries, errors)
-
- def parse(text: String, start: Isar_Token.Pos = Isar_Token.Pos.start): Entries = {
- val entries = new mutable.ListBuffer[Entry]
- var pos = start
- var err_line = 0
-
- try {
- for (chunk <- Bibtex.parse(text)) {
- val pos1 = pos.advance(chunk.source)
- if (chunk.name != "" && !chunk.is_command) {
- entries += Entry(chunk.name, pos.position(pos1.offset))
- }
- if (chunk.is_malformed && err_line == 0) { err_line = pos.line }
- pos = pos1
- }
-
- val err_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))
-
- apply(entries.toList, errors = errors)
- }
- catch { case ERROR(msg) => apply(Nil, errors = List(msg)) }
- }
- }
-
- final class Entries private(val entries: List[Entry], val errors: List[String]) {
- override def toString: String = "Bibtex.Entries(" + entries.length + ")"
-
- def ::: (other: Entries): Entries =
- new Entries(other.entries ::: entries, other.errors ::: errors)
- }
-
- object Session_Entries extends Scala.Fun("bibtex_session_entries") {
- val here = Scala_Project.here
-
- override def invoke(session: Session, args: List[Bytes]): List[Bytes] = {
- val sessions = session.resources.sessions_structure
- val id = Value.Long.parse(Library.the_single(args).text)
- val qualifier =
- session.get_state().lookup_id(id) match {
- case None => Sessions.DRAFT
- case Some(st) => sessions.theory_qualifier(st.command.node_name.theory)
- }
- val res =
- if (qualifier == Sessions.DRAFT || !sessions.defined(qualifier)) Nil
- else qualifier :: sessions(qualifier).bibtex_entries.entries.map(_.encode)
- res.map(Bytes.apply)
- }
- }
-
-
-
- /** content **/
-
- private val months = List(
- "jan",
- "feb",
- "mar",
- "apr",
- "may",
- "jun",
- "jul",
- "aug",
- "sep",
- "oct",
- "nov",
- "dec")
- def is_month(s: String): Boolean = months.contains(s.toLowerCase)
-
- private val commands = List("preamble", "string")
- def is_command(s: String): Boolean = commands.contains(s.toLowerCase)
-
- sealed case class Entry_Type(
- kind: String,
- required: List[String],
- optional_crossref: List[String],
- optional_other: List[String]
- ) {
- val optional_standard: List[String] = List("url", "doi", "ee")
-
- def is_required(s: String): Boolean = required.contains(s.toLowerCase)
- def is_optional(s: String): Boolean =
- optional_crossref.contains(s.toLowerCase) ||
- optional_other.contains(s.toLowerCase) ||
- optional_standard.contains(s.toLowerCase)
-
- def fields: List[String] =
- required ::: optional_crossref ::: optional_other ::: optional_standard
-
- def template: String =
- "@" + kind + "{,\n" + fields.map(x => " " + x + " = {},\n").mkString + "}\n"
- }
-
- val known_entries: List[Entry_Type] =
- List(
- Entry_Type("Article",
- List("author", "title"),
- List("journal", "year"),
- List("volume", "number", "pages", "month", "note")),
- Entry_Type("InProceedings",
- List("author", "title"),
- List("booktitle", "year"),
- List("editor", "volume", "number", "series", "pages", "month", "address",
- "organization", "publisher", "note")),
- Entry_Type("InCollection",
- List("author", "title", "booktitle"),
- List("publisher", "year"),
- List("editor", "volume", "number", "series", "type", "chapter", "pages",
- "edition", "month", "address", "note")),
- Entry_Type("InBook",
- List("author", "editor", "title", "chapter"),
- List("publisher", "year"),
- List("volume", "number", "series", "type", "address", "edition", "month", "pages", "note")),
- Entry_Type("Proceedings",
- List("title", "year"),
- List(),
- List("booktitle", "editor", "volume", "number", "series", "address", "month",
- "organization", "publisher", "note")),
- Entry_Type("Book",
- List("author", "editor", "title"),
- List("publisher", "year"),
- List("volume", "number", "series", "address", "edition", "month", "note")),
- Entry_Type("Booklet",
- List("title"),
- List(),
- List("author", "howpublished", "address", "month", "year", "note")),
- Entry_Type("PhdThesis",
- List("author", "title", "school", "year"),
- List(),
- List("type", "address", "month", "note")),
- Entry_Type("MastersThesis",
- List("author", "title", "school", "year"),
- List(),
- List("type", "address", "month", "note")),
- Entry_Type("TechReport",
- List("author", "title", "institution", "year"),
- List(),
- List("type", "number", "address", "month", "note")),
- Entry_Type("Manual",
- List("title"),
- List(),
- List("author", "organization", "address", "edition", "month", "year", "note")),
- Entry_Type("Unpublished",
- List("author", "title", "note"),
- List(),
- List("month", "year")),
- Entry_Type("Misc",
- List(),
- List(),
- List("author", "title", "howpublished", "month", "year", "note")))
-
- def known_entry(kind: String): Option[Entry_Type] =
- known_entries.find(entry => entry.kind.toLowerCase == kind.toLowerCase)
-
-
-
- /** tokens and chunks **/
-
- object Token {
- object Kind extends Enumeration {
- val COMMAND = Value("command")
- val ENTRY = Value("entry")
- val KEYWORD = Value("keyword")
- val NAT = Value("natural number")
- val STRING = Value("string")
- val NAME = Value("name")
- val IDENT = Value("identifier")
- val SPACE = Value("white space")
- val COMMENT = Value("ignored text")
- val ERROR = Value("bad input")
- }
- }
-
- sealed case class Token(kind: Token.Kind.Value, source: String) {
- def is_kind: Boolean =
- kind == Token.Kind.COMMAND ||
- kind == Token.Kind.ENTRY ||
- kind == Token.Kind.IDENT
- def is_name: Boolean =
- kind == Token.Kind.NAME ||
- kind == Token.Kind.IDENT
- def is_ignored: Boolean =
- kind == Token.Kind.SPACE ||
- kind == Token.Kind.COMMENT
- def is_malformed: Boolean =
- kind == Token.Kind.ERROR
- def is_open: Boolean =
- kind == Token.Kind.KEYWORD && (source == "{" || source == "(")
- }
-
- case class Chunk(kind: String, tokens: List[Token]) {
- val source: String = tokens.map(_.source).mkString
-
- private val content: Option[List[Token]] =
- tokens match {
- case Token(Token.Kind.KEYWORD, "@") :: body if body.nonEmpty =>
- (body.init.filterNot(_.is_ignored), body.last) match {
- case (tok :: Token(Token.Kind.KEYWORD, "{") :: toks, Token(Token.Kind.KEYWORD, "}"))
- if tok.is_kind => Some(toks)
-
- case (tok :: Token(Token.Kind.KEYWORD, "(") :: toks, Token(Token.Kind.KEYWORD, ")"))
- if tok.is_kind => Some(toks)
-
- case _ => None
- }
- case _ => None
- }
-
- def name: String =
- content match {
- case Some(tok :: _) if tok.is_name => tok.source
- case _ => ""
- }
-
- def heading_length: Int =
- if (name == "") 1
- else {
- tokens.takeWhile(tok => !tok.is_open).foldLeft(0) { case (n, tok) => n + tok.source.length }
- }
-
- def is_ignored: Boolean = kind == "" && tokens.forall(_.is_ignored)
- def is_malformed: Boolean = tokens.exists(_.is_malformed)
- def is_command: Boolean = Bibtex.is_command(kind) && name != "" && content.isDefined
- def is_entry: Boolean = Bibtex.known_entry(kind).isDefined && name != "" && content.isDefined
- }
-
-
-
- /** parsing **/
-
- // context of partial line-oriented scans
- abstract class Line_Context
- case object Ignored extends Line_Context
- case object At extends Line_Context
- case class Item_Start(kind: String) extends Line_Context
- case class Item_Open(kind: String, end: String) extends Line_Context
- case class Item(kind: String, end: String, delim: Delimited) extends Line_Context
-
- case class Delimited(quoted: Boolean, depth: Int)
- val Closed: Delimited = Delimited(false, 0)
-
- private def token(kind: Token.Kind.Value)(source: String): Token = Token(kind, source)
- private def keyword(source: String): Token = Token(Token.Kind.KEYWORD, source)
-
-
- // See also https://ctan.org/tex-archive/biblio/bibtex/base/bibtex.web
- // module @<Scan for and process a \.{.bib} command or database entry@>.
-
- object Parsers extends RegexParsers {
- /* white space and comments */
-
- override val whiteSpace = "".r
-
- private val space = """[ \t\n\r]+""".r ^^ token(Token.Kind.SPACE)
- private val spaces = rep(space)
-
-
- /* ignored text */
-
- private val ignored: Parser[Chunk] =
- rep1("""(?i)([^@]+|@[ \t]*comment)""".r) ^^ {
- case ss => Chunk("", List(Token(Token.Kind.COMMENT, ss.mkString))) }
-
- private def ignored_line: Parser[(Chunk, Line_Context)] =
- ignored ^^ { case a => (a, Ignored) }
-
-
- /* delimited string: outermost "..." or {...} and body with balanced {...} */
-
- // see also bibtex.web: scan_a_field_token_and_eat_white, scan_balanced_braces
- private def delimited_depth(delim: Delimited): Parser[(String, Delimited)] =
- new Parser[(String, Delimited)] {
- require(if (delim.quoted) delim.depth > 0 else delim.depth >= 0,
- "bad delimiter depth")
-
- def apply(in: Input): ParseResult[(String, Delimited)] = {
- val start = in.offset
- val end = in.source.length
-
- var i = start
- var q = delim.quoted
- var d = delim.depth
- var finished = false
- while (!finished && i < end) {
- val c = in.source.charAt(i)
-
- if (c == '"' && d == 0) { i += 1; d = 1; q = true }
- else if (c == '"' && d == 1 && q) {
- i += 1; d = 0; q = false; finished = true
- }
- else if (c == '{') { i += 1; d += 1 }
- else if (c == '}') {
- if (d == 1 && !q || d > 1) { i += 1; d -= 1; if (d == 0) finished = true }
- else {i = start; finished = true }
- }
- else if (d > 0) i += 1
- else finished = true
- }
- if (i == start) Failure("bad input", in)
- else {
- val s = in.source.subSequence(start, i).toString
- Success((s, Delimited(q, d)), in.drop(i - start))
- }
- }
- }.named("delimited_depth")
-
- private def delimited: Parser[Token] =
- delimited_depth(Closed) ^?
- { case (s, delim) if delim == Closed => Token(Token.Kind.STRING, s) }
-
- private def recover_delimited: Parser[Token] =
- """["{][^@]*""".r ^^ token(Token.Kind.ERROR)
-
- def delimited_line(ctxt: Item): Parser[(Chunk, Line_Context)] =
- delimited_depth(ctxt.delim) ^^ { case (s, delim1) =>
- (Chunk(ctxt.kind, List(Token(Token.Kind.STRING, s))), ctxt.copy(delim = delim1)) } |
- recover_delimited ^^ { case a => (Chunk(ctxt.kind, List(a)), Ignored) }
-
-
- /* other tokens */
-
- private val at = "@" ^^ keyword
-
- private val nat = "[0-9]+".r ^^ token(Token.Kind.NAT)
-
- private val name = """[\x21-\x7f&&[^"#%'(),={}]]+""".r ^^ token(Token.Kind.NAME)
-
- private val identifier =
- """[\x21-\x7f&&[^"#%'(),={}0-9]][\x21-\x7f&&[^"#%'(),={}]]*""".r
-
- private val ident = identifier ^^ token(Token.Kind.IDENT)
-
- val other_token: Parser[Token] = "[=#,]".r ^^ keyword | (nat | (ident | space))
-
-
- /* body */
-
- private val body =
- delimited | (recover_delimited | other_token)
-
- private def body_line(ctxt: Item) =
- if (ctxt.delim.depth > 0)
- delimited_line(ctxt)
- else
- delimited_line(ctxt) |
- other_token ^^ { case a => (Chunk(ctxt.kind, List(a)), ctxt) } |
- ctxt.end ^^ { case a => (Chunk(ctxt.kind, List(keyword(a))), Ignored) }
-
-
- /* items: command or entry */
-
- private val item_kind =
- identifier ^^ { case a =>
- val kind =
- if (is_command(a)) Token.Kind.COMMAND
- else if (known_entry(a).isDefined) Token.Kind.ENTRY
- else Token.Kind.IDENT
- Token(kind, a)
- }
-
- private val item_begin =
- "{" ^^ { case a => ("}", keyword(a)) } |
- "(" ^^ { case a => (")", keyword(a)) }
-
- private def item_name(kind: String) =
- kind.toLowerCase match {
- case "preamble" => failure("")
- case "string" => identifier ^^ token(Token.Kind.NAME)
- case _ => name
- }
-
- private val item_start =
- at ~ spaces ~ item_kind ~ spaces ^^
- { case a ~ b ~ c ~ d => (c.source, List(a) ::: b ::: List(c) ::: d) }
-
- private val item: Parser[Chunk] =
- (item_start ~ item_begin ~ spaces) into
- { case (kind, a) ~ ((end, b)) ~ c =>
- opt(item_name(kind)) ~ rep(body) ~ opt(end ^^ keyword) ^^ {
- case d ~ e ~ f => Chunk(kind, a ::: List(b) ::: c ::: d.toList ::: e ::: f.toList) } }
-
- private val recover_item: Parser[Chunk] =
- at ~ "[^@]*".r ^^ { case a ~ b => Chunk("", List(a, Token(Token.Kind.ERROR, b))) }
-
-
- /* chunks */
-
- val chunk: Parser[Chunk] = ignored | (item | recover_item)
-
- def chunk_line(ctxt: Line_Context): Parser[(Chunk, Line_Context)] = {
- ctxt match {
- case Ignored =>
- ignored_line |
- at ^^ { case a => (Chunk("", List(a)), At) }
-
- case At =>
- space ^^ { case a => (Chunk("", List(a)), ctxt) } |
- item_kind ^^ { case a => (Chunk(a.source, List(a)), Item_Start(a.source)) } |
- recover_item ^^ { case a => (a, Ignored) } |
- ignored_line
-
- case Item_Start(kind) =>
- space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
- item_begin ^^ { case (end, a) => (Chunk(kind, List(a)), Item_Open(kind, end)) } |
- recover_item ^^ { case a => (a, Ignored) } |
- ignored_line
-
- case Item_Open(kind, end) =>
- space ^^ { case a => (Chunk(kind, List(a)), ctxt) } |
- item_name(kind) ^^ { case a => (Chunk(kind, List(a)), Item(kind, end, Closed)) } |
- body_line(Item(kind, end, Closed)) |
- ignored_line
-
- case item_ctxt: Item =>
- body_line(item_ctxt) |
- ignored_line
-
- case _ => failure("")
- }
- }
- }
-
-
- /* parse */
-
- def parse(input: CharSequence): List[Chunk] =
- Parsers.parseAll(Parsers.rep(Parsers.chunk), Scan.char_reader(input)) match {
- case Parsers.Success(result, _) => result
- case _ => error("Unexpected failure to parse input:\n" + input.toString)
- }
-
- def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) = {
- var in: Reader[Char] = Scan.char_reader(input)
- val chunks = new mutable.ListBuffer[Chunk]
- var ctxt = context
- while (!in.atEnd) {
- val result = Parsers.parse(Parsers.chunk_line(ctxt), in)
- (result : @unchecked) match {
- case Parsers.Success((x, c), rest) => chunks += x; ctxt = c; in = rest
- case Parsers.NoSuccess(_, rest) =>
- error("Unepected failure to parse input:\n" + rest.source.toString)
- }
- }
- (chunks.toList, ctxt)
- }
-
-
-
- /** HTML output **/
-
- private val output_styles =
- List(
- "" -> "html-n",
- "plain" -> "html-n",
- "alpha" -> "html-a",
- "named" -> "html-n",
- "paragraph" -> "html-n",
- "unsort" -> "html-u",
- "unsortlist" -> "html-u")
-
- def html_output(bib: List[Path],
- title: String = "Bibliography",
- body: Boolean = false,
- citations: List[String] = List("*"),
- style: String = "",
- chronological: Boolean = false
- ): String = {
- Isabelle_System.with_tmp_dir("bibtex") { tmp_dir =>
- /* database files */
-
- val bib_files = bib.map(_.drop_ext)
- val bib_names = {
- val names0 = bib_files.map(_.file_name)
- if (Library.duplicates(names0).isEmpty) names0
- else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name })
- }
-
- for ((a, b) <- bib_files zip bib_names) {
- Isabelle_System.copy_file(a.bib, tmp_dir + Path.basic(b).bib)
- }
-
-
- /* style file */
-
- val bst =
- output_styles.toMap.get(style) match {
- case Some(base) => base + (if (chronological) "c" else "") + ".bst"
- case None =>
- error("Bad style for bibtex HTML output: " + quote(style) +
- "\n(expected: " + commas_quote(output_styles.map(_._1)) + ")")
- }
- Isabelle_System.copy_file(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir)
-
-
- /* result */
-
- val in_file = Path.explode("bib.aux")
- val out_file = Path.explode("bib.html")
-
- File.write(tmp_dir + in_file,
- bib_names.mkString("\\bibdata{", ",", "}\n") +
- citations.map(cite => "\\citation{" + cite + "}\n").mkString)
-
- Isabelle_System.bash(
- "\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" +
- " -u -s " + Bash.string(proper_string(style) getOrElse "empty") +
- (if (chronological) " -c" else "") +
- if_proper(title, " -h " + Bash.string(title) + " ") +
- " " + File.bash_path(in_file) + " " + File.bash_path(out_file),
- cwd = tmp_dir.file).check
-
- val html = File.read(tmp_dir + out_file)
-
- if (body) {
- cat_lines(
- split_lines(html).
- dropWhile(line => !line.startsWith("<!-- BEGIN BIBLIOGRAPHY")).reverse.
- dropWhile(line => !line.startsWith("<!-- END BIBLIOGRAPHY")).reverse)
- }
- else html
- }
- }
-
-
-
- /** cite commands and antiquotations **/
-
- /* cite commands */
-
- def cite_commands(options: Options): List[String] =
- space_explode(',', options.string("document_cite_commands"))
-
- val CITE = "cite"
- val NOCITE = "nocite"
-
-
- /* citations within theory source */
-
- object Cite {
- def unapply(tree: XML.Tree): Option[Inner] =
- tree match {
- case XML.Elem(Markup(Markup.Latex_Cite.name, props), body) =>
- val kind = Markup.Kind.unapply(props).getOrElse(CITE)
- val citations = Markup.Citations.get(props)
- val pos = props.filter(Markup.position_property)
- Some(Inner(kind, citations, body, pos))
- case _ => None
- }
-
- sealed case class Inner(kind: String, citations: String, location: XML.Body, pos: Position.T) {
- def nocite: Inner = copy(kind = NOCITE, location = Nil)
-
- def latex_text: Latex.Text = {
- val props =
- (if (kind.nonEmpty) Markup.Kind(kind) else Nil) :::
- Markup.Citations(citations) ::: pos
- List(XML.Elem(Markup.Latex_Cite(props), location))
- }
-
- override def toString: String = citations
- }
-
- sealed case class Outer(kind: String, body: String, start: Isar_Token.Pos) {
- def pos: Position.T = start.position()
-
- def parse: Option[Inner] = {
- val tokens = Isar_Token.explode(Parsers.keywords, body)
- Parsers.parse_all(Parsers.inner(pos), Isar_Token.reader(tokens, start)) match {
- case Parsers.Success(res, _) => Some(res)
- case _ => None
- }
- }
-
- def errors: List[String] =
- if (parse.isDefined) Nil
- else List("Malformed citation" + Position.here(pos))
-
- override def toString: String =
- parse match {
- case Some(inner) => inner.toString
- case None => "<malformed>"
- }
- }
-
- object Parsers extends Parse.Parsers {
- val keywords: Keyword.Keywords = Thy_Header.bootstrap_keywords + "in" + "using"
-
- val location: Parser[String] = embedded ~ $$$("in") ^^ { case x ~ _ => x } | success("")
- val citations: Parser[String] = rep1sep(name, $$$("and")) ^^ (x => x.mkString(","))
- val kind: Parser[String] = $$$("using") ~! name ^^ { case _ ~ x => x } | success(CITE)
-
- def inner(pos: Position.T): Parser[Inner] =
- location ~ citations ~ kind ^^
- { case x ~ y ~ z => Inner(z, y, XML.string(x), pos) }
- }
-
- def parse(
- cite_commands: List[String],
- text: String,
- start: Isar_Token.Pos = Isar_Token.Pos.start
- ): List[Outer] = {
- val controls = cite_commands.map(s => Symbol.control_prefix + s + Symbol.control_suffix)
- val special = (controls ::: controls.map(Symbol.decode)).toSet
-
- val Parsers = Antiquote.Parsers
- Parsers.parseAll(Parsers.rep(Parsers.antiquote_special(special)), text) match {
- case Parsers.Success(ants, _) =>
- var pos = start
- val result = new mutable.ListBuffer[Outer]
- for (ant <- ants) {
- ant match {
- case Antiquote.Control(source) =>
- for {
- head <- Symbol.iterator(source).nextOption
- kind <- Symbol.control_name(Symbol.encode(head))
- } {
- val rest = source.substring(head.length)
- val (body, pos1) =
- if (rest.isEmpty) (rest, pos)
- else (Scan.Parsers.cartouche_content(rest), pos.advance(Symbol.open))
- result += Outer(kind, body, pos1)
- }
- case _ =>
- }
- pos = pos.advance(ant.source)
- }
- result.toList
- case _ => error("Unexpected failure parsing special antiquotations:\n" + text)
- }
- }
- }
-
-
- /* update old forms: @{cite ...} and \cite{...} */
-
- def cite_antiquotation(name: String, body: String): String =
- """\<^""" + name + """>\<open>""" + body + """\<close>"""
-
- def cite_antiquotation(name: String, location: String, citations: List[String]): String = {
- val body =
- if_proper(location, Symbol.cartouche(location) + " in ") +
- citations.map(quote).mkString(" and ")
- cite_antiquotation(name, body)
- }
-
- private val Cite_Command = """\\(cite|nocite|citet|citep)((?:\[[^\]]*\])?)\{([^}]*)\}""".r
- private val Cite_Macro = """\[\s*cite_macro\s*=\s*"?(\w+)"?\]\s*""".r
-
- def update_cite_commands(str: String): String =
- Cite_Command.replaceAllIn(str, { m =>
- val name = m.group(1)
- val loc = m.group(2)
- val location =
- if (loc.startsWith("[") && loc.endsWith("]")) loc.substring(1, loc.length - 1)
- else loc
- val citations = space_explode(',', m.group(3)).map(_.trim)
- Regex.quoteReplacement(cite_antiquotation(name, location, citations))
- })
-
- def update_cite_antiquotation(cite_commands: List[String], str: String): String = {
- val opt_body =
- for {
- str1 <- Library.try_unprefix("@{cite", str)
- str2 <- Library.try_unsuffix("}", str1)
- } yield str2.trim
-
- opt_body match {
- case None => str
- case Some(body0) =>
- val (name, body1) =
- Cite_Macro.findFirstMatchIn(body0) match {
- case None => (CITE, body0)
- case Some(m) => (m.group(1), Cite_Macro.replaceAllIn(body0, ""))
- }
- val body2 = body1.replace("""\<close>""", """\<close> in""")
- if (cite_commands.contains(name)) cite_antiquotation(name, body2)
- else cite_antiquotation(CITE, body2 + " using " + quote(name))
- }
- }
-}
--- a/src/Pure/Thy/latex.ML Sat Jan 20 15:07:41 2024 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,262 +0,0 @@
-(* Title: Pure/Thy/latex.ML
- Author: Makarius
-
-LaTeX output of theory sources.
-*)
-
-signature LATEX =
-sig
- type text = XML.body
- val text: string * Position.T -> text
- val string: string -> text
- val block: text -> XML.tree
- val output: text -> text
- val macro0: string -> text
- val macro: string -> text -> text
- val environment: string -> text -> text
- val output_name: string -> string
- val output_ascii: string -> string
- val output_ascii_breakable: string -> string -> string
- val output_symbols: Symbol.symbol list -> string
- val output_syms: string -> string
- val symbols: Symbol_Pos.T list -> text
- val symbols_output: Symbol_Pos.T list -> text
- val isabelle_body: string -> text -> text
- val theory_entry: string -> string
- val cite: {kind: string, citations: (string * Position.T) list, location: text} -> text
- type index_item = {text: text, like: string}
- type index_entry = {items: index_item list, def: bool}
- val index_entry: index_entry -> text
- val index_variants: (binding -> bool option -> 'a -> 'a) -> binding -> 'a -> 'a
- val latexN: string
- val latex_markup: string * Properties.T -> Markup.output
-end;
-
-structure Latex: LATEX =
-struct
-
-(* text with positions *)
-
-type text = XML.body;
-
-fun text (s, pos) =
- if s = "" then []
- else if pos = Position.none then [XML.Text s]
- else [XML.Elem (Position.markup pos Markup.document_latex, [XML.Text s])];
-
-fun string s = text (s, Position.none);
-
-fun block body = XML.Elem (Markup.document_latex, body);
-
-fun output body = [XML.Elem (Markup.latex_output, body)];
-
-fun macro0 name = [XML.Elem (Markup.latex_macro0 name, [])];
-fun macro name body = [XML.Elem (Markup.latex_macro name, body)];
-fun environment name body = [XML.Elem (Markup.latex_environment name, body)];
-
-
-(* output name for LaTeX macros *)
-
-val output_name =
- translate_string
- (fn "_" => "UNDERSCORE"
- | "'" => "PRIME"
- | "0" => "ZERO"
- | "1" => "ONE"
- | "2" => "TWO"
- | "3" => "THREE"
- | "4" => "FOUR"
- | "5" => "FIVE"
- | "6" => "SIX"
- | "7" => "SEVEN"
- | "8" => "EIGHT"
- | "9" => "NINE"
- | s => s);
-
-fun enclose_name bg en = enclose bg en o output_name;
-
-
-(* output verbatim ASCII *)
-
-val output_ascii =
- translate_string
- (fn " " => "\\ "
- | "\t" => "\\ "
- | "\n" => "\\isanewline\n"
- | s =>
- s
- |> member_string "\"#$%&',-<>\\^_`{}~" s ? enclose "{\\char`\\" "}"
- |> suffix "{\\kern0pt}");
-
-fun output_ascii_breakable sep =
- space_explode sep
- #> map output_ascii
- #> space_implode (output_ascii sep ^ "\\discretionary{}{}{}");
-
-
-(* output symbols *)
-
-local
-
-val char_table =
- Symtab.make
- [("\007", "{\\isacharbell}"),
- ("!", "{\\isacharbang}"),
- ("\"", "{\\isachardoublequote}"),
- ("#", "{\\isacharhash}"),
- ("$", "{\\isachardollar}"),
- ("%", "{\\isacharpercent}"),
- ("&", "{\\isacharampersand}"),
- ("'", "{\\isacharprime}"),
- ("(", "{\\isacharparenleft}"),
- (")", "{\\isacharparenright}"),
- ("*", "{\\isacharasterisk}"),
- ("+", "{\\isacharplus}"),
- (",", "{\\isacharcomma}"),
- ("-", "{\\isacharminus}"),
- (".", "{\\isachardot}"),
- ("/", "{\\isacharslash}"),
- (":", "{\\isacharcolon}"),
- (";", "{\\isacharsemicolon}"),
- ("<", "{\\isacharless}"),
- ("=", "{\\isacharequal}"),
- (">", "{\\isachargreater}"),
- ("?", "{\\isacharquery}"),
- ("@", "{\\isacharat}"),
- ("[", "{\\isacharbrackleft}"),
- ("\\", "{\\isacharbackslash}"),
- ("]", "{\\isacharbrackright}"),
- ("^", "{\\isacharcircum}"),
- ("_", "{\\isacharunderscore}"),
- ("`", "{\\isacharbackquote}"),
- ("{", "{\\isacharbraceleft}"),
- ("|", "{\\isacharbar}"),
- ("}", "{\\isacharbraceright}"),
- ("~", "{\\isachartilde}")];
-
-fun output_chr " " = "\\ "
- | output_chr "\t" = "\\ "
- | output_chr "\n" = "\\isanewline\n"
- | output_chr c =
- (case Symtab.lookup char_table c of
- SOME s => s ^ "{\\kern0pt}"
- | NONE => if Symbol.is_ascii_digit c then enclose "{\\isadigit{" "}}" c else c);
-
-fun output_sym sym =
- (case Symbol.decode sym of
- Symbol.Char s => output_chr s
- | Symbol.UTF8 s => s
- | Symbol.Sym s => enclose_name "{\\isasym" "}" s
- | Symbol.Control s => enclose_name "\\isactrl" " " s
- | Symbol.Malformed s => error (Symbol.malformed_msg s)
- | Symbol.EOF => error "Bad EOF symbol");
-
-open Basic_Symbol_Pos;
-
-val scan_latex_length =
- Scan.many1 (fn (s, _) => s <> Symbol.latex andalso Symbol.not_eof s)
- >> (Symbol.length o map Symbol_Pos.symbol) ||
- $$ Symbol.latex -- Scan.option (Scan.permissive Symbol_Pos.scan_cartouche "") >> K 0;
-
-val scan_latex =
- $$ Symbol.latex |-- Symbol_Pos.scan_cartouche_content "Embedded LaTeX: "
- >> (implode o map Symbol_Pos.symbol) ||
- Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_sym o Symbol_Pos.symbol);
-
-fun read scan syms =
- Scan.read Symbol_Pos.stopper (Scan.repeat scan) (map (rpair Position.none) syms);
-
-in
-
-val length_symbols =
- Integer.build o fold Integer.add o these o read scan_latex_length;
-
-fun output_symbols syms =
- if member (op =) syms Symbol.latex then
- (case read scan_latex syms of
- SOME ss => implode ss
- | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms)))
- else implode (map output_sym syms);
-
-val output_syms = output_symbols o Symbol.explode;
-
-end;
-
-fun symbols syms = text (Symbol_Pos.content syms, #1 (Symbol_Pos.range syms));
-fun symbols_output syms =
- text (output_symbols (map Symbol_Pos.symbol syms), #1 (Symbol_Pos.range syms));
-
-
-(* theory presentation *)
-
-fun isabelle_body name =
- XML.enclose
- ("%\n\\begin{isabellebody}%\n\\setisabellecontext{" ^ output_syms name ^ "}%\n")
- "%\n\\end{isabellebody}%\n";
-
-fun theory_entry name = "\\input{" ^ name ^ ".tex}\n\n";
-
-
-(* cite: references to bibliography *)
-
-fun cite {kind, location, citations} =
- let
- val _ =
- citations |> List.app (fn (s, pos) =>
- if member_string s ","
- then error ("Single citation expected, without commas" ^ Position.here pos)
- else ());
- val citations' = space_implode "," (map #1 citations);
- val markup = Markup.latex_cite {kind = kind, citations = citations'};
- in [XML.Elem (markup, location)] end;
-
-
-(* index entries *)
-
-type index_item = {text: text, like: string};
-type index_entry = {items: index_item list, def: bool};
-
-fun index_item (item: index_item) =
- XML.wrap_elem ((Markup.latex_index_item, #text item), XML.string (#like item));
-
-fun index_entry (entry: index_entry) =
- [XML.Elem (Markup.latex_index_entry (if #def entry then "isaindexdef" else "isaindexref"),
- map index_item (#items entry))];
-
-fun index_binding NONE = I
- | index_binding (SOME def) = Binding.map_name (suffix (if def then "_def" else "_ref"));
-
-fun index_variants setup binding =
- fold (fn index => setup (index_binding index binding) index) [NONE, SOME true, SOME false];
-
-
-(* print mode *)
-
-val latexN = "latex";
-
-local
-
-fun latex_output str =
- let val syms = Symbol.explode str
- in (output_symbols syms, length_symbols syms) end;
-
-val command_markup = YXML.output_markup (Markup.latex_macro "isacommand");
-val keyword_markup = YXML.output_markup (Markup.latex_macro "isakeyword");
-val indent_markup = YXML.output_markup (Markup.latex_macro "isaindent");
-
-in
-
-fun latex_markup (s, _: Properties.T) =
- if member (op =) [Markup.commandN, Markup.keyword1N, Markup.keyword3N] s then command_markup
- else if s = Markup.keyword2N then keyword_markup
- else Markup.no_output;
-
-val _ = Output.add_mode latexN latex_output (prefix Symbol.latex o cartouche);
-val _ = Markup.add_mode latexN latex_markup;
-
-val _ = Pretty.add_mode latexN
- (fn s => fn _ => if s = "" then s else uncurry enclose indent_markup s);
-
-end;
-
-end;
--- a/src/Pure/Thy/latex.scala Sat Jan 20 15:07:41 2024 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,469 +0,0 @@
-/* Title: Pure/Thy/latex.scala
- Author: Makarius
-
-Support for LaTeX.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile}
-
-import scala.annotation.tailrec
-import scala.collection.mutable
-import scala.collection.immutable.TreeMap
-import scala.util.matching.Regex
-
-
-object Latex {
- /* output name for LaTeX macros */
-
- private val output_name_map: Map[Char, String] =
- Map('_' -> "UNDERSCORE",
- '\'' -> "PRIME",
- '0' -> "ZERO",
- '1' -> "ONE",
- '2' -> "TWO",
- '3' -> "THREE",
- '4' -> "FOUR",
- '5' -> "FIVE",
- '6' -> "SIX",
- '7' -> "SEVEN",
- '8' -> "EIGHT",
- '9' -> "NINE")
-
- def output_name(name: String): String =
- if (name.exists(output_name_map.keySet)) {
- val res = new StringBuilder
- for (c <- name) {
- output_name_map.get(c) match {
- case None => res += c
- case Some(s) => res ++= s
- }
- }
- res.toString
- }
- else name
-
-
- /* index entries */
-
- def index_escape(str: String): String = {
- val special1 = "!\"@|"
- val special2 = "\\{}#"
- if (str.exists(c => special1.contains(c) || special2.contains(c))) {
- val res = new StringBuilder
- for (c <- str) {
- if (special1.contains(c)) {
- res ++= "\\char"
- res ++= Value.Int(c)
- }
- else {
- if (special2.contains(c)) { res += '"'}
- res += c
- }
- }
- res.toString
- }
- else str
- }
-
- object Index_Item {
- sealed case class Value(text: Text, like: String)
- def unapply(tree: XML.Tree): Option[Value] =
- tree match {
- case XML.Wrapped_Elem(Markup.Latex_Index_Item(_), text, like) =>
- Some(Value(text, XML.content(like)))
- case _ => None
- }
- }
-
- object Index_Entry {
- sealed case class Value(items: List[Index_Item.Value], kind: String)
- def unapply(tree: XML.Tree): Option[Value] =
- tree match {
- case XML.Elem(Markup.Latex_Index_Entry(kind), body) =>
- val items = body.map(Index_Item.unapply)
- if (items.forall(_.isDefined)) Some(Value(items.map(_.get), kind)) else None
- case _ => None
- }
- }
-
-
- /* tags */
-
- object Tags {
- enum Op { case fold, drop, keep }
-
- val standard = "document,theory,proof,ML,visible,-invisible,important,unimportant"
-
- private def explode(spec: String): List[String] = space_explode(',', spec)
-
- def apply(spec: String): Tags =
- new Tags(spec,
- (explode(standard) ::: explode(spec)).foldLeft(TreeMap.empty[String, Op]) {
- case (m, tag) =>
- tag.toList match {
- case '/' :: cs => m + (cs.mkString -> Op.fold)
- case '-' :: cs => m + (cs.mkString -> Op.drop)
- case '+' :: cs => m + (cs.mkString -> Op.keep)
- case cs => m + (cs.mkString -> Op.keep)
- }
- })
-
- val empty: Tags = apply("")
- }
-
- class Tags private(spec: String, map: TreeMap[String, Tags.Op]) {
- override def toString: String = spec
-
- def get(name: String): Option[Tags.Op] = map.get(name)
-
- def sty(comment_latex: Boolean): File.Content = {
- val path = Path.explode("isabelletags.sty")
- val comment =
- if (comment_latex) """\usepackage{comment}"""
- else """%plain TeX version of comment package -- much faster!
-\let\isafmtname\fmtname\def\fmtname{plain}
-\usepackage{comment}
-\let\fmtname\isafmtname"""
- val tags =
- (for ((name, op) <- map.iterator)
- yield "\\isa" + op + "tag{" + name + "}").toList
- File.content(path, comment + """
-
-\newcommand{\isakeeptag}[1]%
-{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
-\newcommand{\isadroptag}[1]%
-{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
-\newcommand{\isafoldtag}[1]%
-{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
-
-""" + terminate_lines(tags))
- }
- }
-
-
- /* output text and positions */
-
- type Text = XML.Body
-
- def position(a: String, b: String): String = "%:%" + a + "=" + b + "%:%\n"
-
- def init_position(file_pos: String): List[String] =
- if (file_pos.isEmpty) Nil
- else List("\\endinput\n", position(Markup.FILE, file_pos))
-
- def append_position(path: Path, file_pos: String): Unit = {
- val pos = init_position(file_pos).mkString
- if (pos.nonEmpty) {
- val sep = if (File.read(path).endsWith("\n")) "" else "\n"
- File.append(path, sep + pos)
- }
- }
-
- def copy_file(src: Path, dst: Path): Unit = {
- Isabelle_System.copy_file(src, dst)
- if (src.is_latex) {
- val target = if (dst.is_dir) dst + src.base else dst
- val file_pos = File.symbolic_path(src)
- append_position(target, file_pos)
- }
- }
-
- def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = {
- Isabelle_System.copy_file_base(base_dir, src, target_dir)
- if (src.is_latex) {
- val file_pos = File.symbolic_path(base_dir + src)
- append_position(target_dir + src, file_pos)
- }
- }
-
- class Output(val options: Options) {
- def latex_output(latex_text: Text): String = make(latex_text)
-
- def latex_macro0(name: String, optional_argument: String = ""): Text =
- XML.string("\\" + name + optional_argument)
-
- def latex_macro(name: String, body: Text, optional_argument: String = ""): Text =
- XML.enclose("\\" + name + optional_argument + "{", "}", body)
-
- def latex_environment(name: String, body: Text, optional_argument: String = ""): Text =
- XML.enclose(
- "%\n\\begin{" + name + "}" + optional_argument + "%\n",
- "%\n\\end{" + name + "}", body)
-
- def latex_heading(kind: String, body: Text, optional_argument: String = ""): Text =
- XML.enclose(
- "%\n\\" + options.string("document_heading_prefix") + kind + optional_argument + "{",
- "%\n}\n", body)
-
- def latex_body(kind: String, body: Text, optional_argument: String = ""): Text =
- latex_environment("isamarkup" + kind, body, optional_argument)
-
- def latex_tag(name: String, body: Text, delim: Boolean = false): Text = {
- val s = output_name(name)
- val kind = if (delim) "delim" else "tag"
- val end = if (delim) "" else "{\\isafold" + s + "}%\n"
- if (options.bool("document_comment_latex")) {
- XML.enclose(
- "%\n\\begin{isa" + kind + s + "}\n",
- "%\n\\end{isa" + kind + s + "}\n" + end, body)
- }
- else {
- XML.enclose(
- "%\n\\isa" + kind + s + "\n",
- "%\n\\endisa" + kind + s + "\n" + end, body)
- }
- }
-
- def cite(inner: Bibtex.Cite.Inner): Text = {
- val body =
- latex_macro0(inner.kind) :::
- (if (inner.location.isEmpty) Nil
- else XML.string("[") ::: inner.location ::: XML.string("]")) :::
- XML.string("{" + inner.citations + "}")
-
- if (inner.pos.isEmpty) body
- else List(XML.Elem(Markup.Latex_Output(inner.pos), body))
- }
-
- def index_item(item: Index_Item.Value): String = {
- val like = if_proper(item.like, index_escape(item.like) + "@")
- val text = index_escape(latex_output(item.text))
- like + text
- }
-
- def index_entry(entry: Index_Entry.Value): Text = {
- val items = entry.items.map(index_item).mkString("!")
- val kind = if_proper(entry.kind, "|" + index_escape(entry.kind))
- latex_macro("index", XML.string(items + kind))
- }
-
-
- /* standard output of text with per-line positions */
-
- def unknown_elem(elem: XML.Elem, pos: Position.T): XML.Body =
- error("Unknown latex markup element " + quote(elem.name) + Position.here(pos) +
- ":\n" + XML.string_of_tree(elem))
-
- def make(
- latex_text: Text,
- file_pos: String = "",
- line_pos: Properties.T => Option[Int] = Position.Line.unapply
- ): String = {
- var line = 1
- val result = new mutable.ListBuffer[String]
- val positions = new mutable.ListBuffer[String] ++= init_position(file_pos)
-
- val file_position = if (file_pos.isEmpty) Position.none else Position.File(file_pos)
-
- def traverse(xml: XML.Body): Unit = {
- xml.foreach {
- case XML.Text(s) =>
- line += Library.count_newlines(s)
- result += s
- case elem @ XML.Elem(markup, body) =>
- val a = Markup.Optional_Argument.get(markup.properties)
- traverse {
- markup match {
- case Markup.Document_Latex(props) =>
- if (positions.nonEmpty) {
- for (l <- line_pos(props)) {
- val s = position(Value.Int(line), Value.Int(l))
- if (positions.last != s) positions += s
- }
- }
- body
- case Markup.Latex_Output(_) => XML.string(latex_output(body))
- case Markup.Latex_Macro0(name) if body.isEmpty => latex_macro0(name, a)
- case Markup.Latex_Macro(name) => latex_macro(name, body, a)
- case Markup.Latex_Environment(name) => latex_environment(name, body, a)
- case Markup.Latex_Heading(kind) => latex_heading(kind, body, a)
- case Markup.Latex_Body(kind) => latex_body(kind, body, a)
- case Markup.Latex_Delim(name) => latex_tag(name, body, delim = true)
- case Markup.Latex_Tag(name) => latex_tag(name, body)
- case Markup.Latex_Cite(_) =>
- elem match {
- case Bibtex.Cite(inner) => cite(inner)
- case _ => unknown_elem(elem, file_position)
- }
- case Markup.Latex_Index_Entry(_) =>
- elem match {
- case Index_Entry(entry) => index_entry(entry)
- case _ => unknown_elem(elem, file_position)
- }
- case _ => unknown_elem(elem, file_position)
- }
- }
- }
- }
- traverse(latex_text)
-
- result ++= positions
- result.mkString
- }
- }
-
-
- /* generated .tex file */
-
- private val File_Pattern = """^%:%file=(.+)%:%$""".r
- private val Line_Pattern = """^*%:%(\d+)=(\d+)%:%$""".r
-
- def read_tex_file(tex_file: Path): Tex_File = {
- val positions =
- Line.logical_lines(File.read(tex_file)).reverse.
- takeWhile(_ != "\\endinput").reverse
-
- val source_file =
- positions match {
- case File_Pattern(file) :: _ => Some(file)
- case _ => None
- }
-
- val source_lines =
- if (source_file.isEmpty) Nil
- else
- positions.flatMap(line =>
- line match {
- case Line_Pattern(Value.Int(line), Value.Int(source_line)) => Some(line -> source_line)
- case _ => None
- })
-
- new Tex_File(tex_file, source_file, source_lines)
- }
-
- final class Tex_File private[Latex](
- tex_file: Path,
- source_file: Option[String],
- source_lines: List[(Int, Int)]
- ) {
- override def toString: String = tex_file.toString
-
- def source_position(l: Int): Option[Position.T] =
- source_file match {
- case None => None
- case Some(file) =>
- val source_line =
- source_lines.iterator.takeWhile({ case (m, _) => m <= l }).
- foldLeft(0) { case (_, (_, n)) => n }
- if (source_line == 0) None else Some(Position.Line_File(source_line, file))
- }
-
- def position(line: Int): Position.T =
- source_position(line) getOrElse
- Position.Line_File(line, source_file.getOrElse(tex_file.implode))
- }
-
-
- /* latex log */
-
- def latex_errors(dir: Path, root_name: String): List[String] = {
- val root_log_path = dir + Path.explode(root_name).log
- if (root_log_path.is_file) {
- for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
- yield "Latex error" + Position.here(pos) + ":\n" + Library.indent_lines(2, msg)
- }
- else Nil
- }
-
- def filter_errors(dir: Path, root_log: String): List[(String, Position.T)] = {
- val seen_files = Synchronized(Map.empty[JFile, Tex_File])
-
- def check_tex_file(path: Path): Option[Tex_File] =
- seen_files.change_result(seen =>
- seen.get(path.file) match {
- case None =>
- if (path.is_file) {
- val tex_file = read_tex_file(path)
- (Some(tex_file), seen + (path.file -> tex_file))
- }
- else (None, seen)
- case some => (some, seen)
- })
-
- def tex_file_position(path: Path, line: Int): Position.T =
- check_tex_file(path) match {
- case Some(tex_file) => tex_file.position(line)
- case None => Position.Line_File(line, path.implode)
- }
-
- object File_Line_Error {
- val Pattern: Regex = """^(.*?\.\w\w\w):(\d+): (.*)$""".r
- def unapply(line: String): Option[(Path, Int, String)] =
- line match {
- case Pattern(file, Value.Int(line), message) =>
- val path = File.standard_path(file)
- if (Path.is_wellformed(path)) {
- val file = (dir + Path.explode(path)).canonical
- val msg = Library.perhaps_unprefix("LaTeX Error: ", message)
- if (file.is_file) Some((file, line, msg)) else None
- }
- else None
- case _ => None
- }
- }
-
- val Line_Error = """^l\.\d+ (.*)$""".r
- val More_Error =
- List(
- "<argument>",
- "<template>",
- "<recently read>",
- "<to be read again>",
- "<inserted text>",
- "<output>",
- "<everypar>",
- "<everymath>",
- "<everydisplay>",
- "<everyhbox>",
- "<everyvbox>",
- "<everyjob>",
- "<everycr>",
- "<mark>",
- "<everyeof>",
- "<write>").mkString("^(?:", "|", ") (.*)$").r
-
- val Bad_Font = """^LaTeX Font Warning: (Font .*\btxmia\b.* undefined).*$""".r
- val Bad_File = """^! LaTeX Error: (File `.*' not found\.)$""".r
-
- val error_ignore =
- Set(
- "See the LaTeX manual or LaTeX Companion for explanation.",
- "Type H <return> for immediate help.")
-
- def error_suffix1(lines: List[String]): Option[String] = {
- val lines1 =
- lines.take(20).takeWhile({ case File_Line_Error((_, _, _)) => false case _ => true })
- lines1.zipWithIndex.collectFirst({
- case (Line_Error(msg), i) =>
- cat_lines(lines1.take(i).filterNot(error_ignore) ::: List(msg)) })
- }
- def error_suffix2(lines: List[String]): Option[String] =
- lines match {
- case More_Error(msg) :: _ => Some(msg)
- case _ => None
- }
-
- @tailrec def filter(
- lines: List[String],
- result: List[(String, Position.T)]
- ) : List[(String, Position.T)] = {
- lines match {
- case File_Line_Error((file, line, msg1)) :: rest1 =>
- val pos = tex_file_position(file, line)
- val msg2 = error_suffix1(rest1) orElse error_suffix2(rest1) getOrElse ""
- filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result)
- case Bad_Font(msg) :: rest =>
- filter(rest, (msg, Position.none) :: result)
- case Bad_File(msg) :: rest =>
- filter(rest, (msg, Position.none) :: result)
- case _ :: rest => filter(rest, result)
- case Nil => result.reverse
- }
- }
-
- filter(Line.logical_lines(root_log), Nil)
- }
-}