src/Pure/Thy/bibtex.scala
changeset 72756 72ac27ea12b2
parent 72729 83411077c37b
child 72836 ec61e1767689
equal deleted inserted replaced
72755:8dffbe01a3e1 72756:72ac27ea12b2
   145     })
   145     })
   146   }
   146   }
   147 
   147 
   148   object Check_Database extends Scala.Fun("bibtex_check_database")
   148   object Check_Database extends Scala.Fun("bibtex_check_database")
   149   {
   149   {
       
   150     val here = Scala_Project.here
   150     def apply(database: String): String =
   151     def apply(database: String): String =
   151     {
   152     {
   152       import XML.Encode._
   153       import XML.Encode._
   153       YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))(
   154       YXML.string_of_body(pair(list(pair(string, properties)), list(pair(string, properties)))(
   154         check_database(database)))
   155         check_database(database)))