merged
authorlammich <lammich@in.tum.de>
Fri Jun 02 09:26:04 2017 +0200 (2017-06-02)
changeset 6600510e5265c2a25
parent 66004 797ef4889177
parent 66002 c85f677cfb0a
child 66006 cec184536dfd
merged
     1.1 --- a/etc/isabelle.css	Thu Jun 01 16:56:05 2017 +0200
     1.2 +++ b/etc/isabelle.css	Fri Jun 02 09:26:04 2017 +0200
     1.3 @@ -1,22 +1,3 @@
     1.4 -/* style file for Isabelle XHTML/XML output */
     1.5 -
     1.6 -@font-face {
     1.7 -  font-family: 'IsabelleText';
     1.8 -  src: url('fonts/IsabelleText.ttf') format('truetype');
     1.9 -}
    1.10 -
    1.11 -@font-face {
    1.12 -  font-family: 'IsabelleText';
    1.13 -  src: url('fonts/IsabelleTextBold.ttf') format('truetype');
    1.14 -  font-weight: bold;
    1.15 -}
    1.16 -
    1.17 -@font-face {
    1.18 -  font-family: 'Vacuous';
    1.19 -  src: url('fonts/Vacuous.ttf') format('truetype');
    1.20 -}
    1.21 -
    1.22 -
    1.23  /* standard document markup */
    1.24  
    1.25  dt {
     2.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Thu Jun 01 16:56:05 2017 +0200
     2.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Fri Jun 02 09:26:04 2017 +0200
     2.3 @@ -955,15 +955,13 @@
     2.4    let
     2.5      val config =
     2.6        {cautious = cautious,
     2.7 -       problem_name =
     2.8 -        SOME (TPTP_Problem_Name.parse_problem_name ((Path.base #> Path.implode)
     2.9 -         file_name))}
    2.10 +       problem_name = SOME (TPTP_Problem_Name.parse_problem_name (Path.base_name file_name))}
    2.11    in interpret_file' config [] path_prefixes file_name end
    2.12  
    2.13  fun import_file cautious path_prefixes file_name type_map const_map thy =
    2.14    let
    2.15      val prob_name =
    2.16 -      TPTP_Problem_Name.parse_problem_name (Path.implode (Path.base file_name))
    2.17 +      TPTP_Problem_Name.parse_problem_name (Path.base_name file_name)
    2.18      val (result, thy') =
    2.19        interpret_file cautious path_prefixes file_name type_map const_map thy
    2.20    (*FIXME doesn't check if problem has already been interpreted*)
     3.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Thu Jun 01 16:56:05 2017 +0200
     3.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Fri Jun 02 09:26:04 2017 +0200
     3.3 @@ -1790,8 +1790,7 @@
     3.4   (on_load : proof_annotation -> theory -> (proof_annotation * theory)) thy =
     3.5    let
     3.6      val prob_name =
     3.7 -      Path.base file_name
     3.8 -      |> Path.implode
     3.9 +      Path.base_name file_name
    3.10        |> TPTP_Problem_Name.parse_problem_name
    3.11      val thy1 = TPTP_Interpret.import_file cautious path_prefixes file_name [] [] thy
    3.12      val fms = get_fmlas_of_prob thy1 prob_name
     4.1 --- a/src/HOL/TPTP/TPTP_Parser_Test.thy	Thu Jun 01 16:56:05 2017 +0200
     4.2 +++ b/src/HOL/TPTP/TPTP_Parser_Test.thy	Fri Jun 02 09:26:04 2017 +0200
     4.3 @@ -47,8 +47,7 @@
     4.4  
     4.5  (*test against all TPTP problems*)
     4.6  fun problem_names () =
     4.7 -    map (Path.base #>
     4.8 -         Path.implode #>
     4.9 +    map (Path.base_name #>
    4.10           TPTP_Problem_Name.parse_problem_name #>
    4.11           TPTP_Problem_Name.mangle_problem_name)
    4.12       (TPTP_Syntax.get_file_list tptp_probs_dir)
     5.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Thu Jun 01 16:56:05 2017 +0200
     5.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Fri Jun 02 09:26:04 2017 +0200
     5.3 @@ -58,7 +58,7 @@
     5.4  
     5.5  val prob_names =
     5.6    probs
     5.7 -  |> map (Path.base #> Path.implode #> TPTP_Problem_Name.Nonstandard)
     5.8 +  |> map (Path.base_name #> TPTP_Problem_Name.Nonstandard)
     5.9  \<close>
    5.10  
    5.11  setup \<open>
    5.12 @@ -575,7 +575,9 @@
    5.13  fun test_partial_reconstruction thy prob_file =
    5.14    let
    5.15      val prob_name =
    5.16 -      (Path.base #> Path.implode #> TPTP_Problem_Name.Nonstandard) prob_file
    5.17 +      prob_file
    5.18 +      |> Path.base_name
    5.19 +      |> TPTP_Problem_Name.Nonstandard
    5.20  
    5.21      val thy' =
    5.22        try
    5.23 @@ -658,8 +660,7 @@
    5.24        val ctxt = Proof_Context.init_global thy' (*FIXME pass ctxt instead of thy*)
    5.25        val prob_name =
    5.26          file
    5.27 -        |> Path.base
    5.28 -        |> Path.implode
    5.29 +        |> Path.base_name
    5.30          |> TPTP_Problem_Name.Nonstandard
    5.31      in
    5.32        Timeout.apply (Time.fromSeconds (if timeout = 0 then 60 else timeout))
     6.1 --- a/src/Pure/Admin/build_history.scala	Thu Jun 01 16:56:05 2017 +0200
     6.2 +++ b/src/Pure/Admin/build_history.scala	Fri Jun 02 09:26:04 2017 +0200
     6.3 @@ -211,7 +211,7 @@
     6.4        val build_end = Date.now()
     6.5  
     6.6        val build_info: Build_Log.Build_Info =
     6.7 -        Build_Log.Log_File(log_path.base.implode, build_result.out_lines).
     6.8 +        Build_Log.Log_File(log_path.base_name, build_result.out_lines).
     6.9            parse_build_info(ml_statistics = true)
    6.10  
    6.11  
    6.12 @@ -489,7 +489,7 @@
    6.13          val log = Path.explode(line)
    6.14          val bytes = ssh.read_bytes(log)
    6.15          ssh.rm(log)
    6.16 -        (log.base.implode, bytes)
    6.17 +        (log.base_name, bytes)
    6.18        }
    6.19      })
    6.20    }
     7.1 --- a/src/Pure/Admin/build_status.scala	Thu Jun 01 16:56:05 2017 +0200
     7.2 +++ b/src/Pure/Admin/build_status.scala	Fri Jun 02 09:26:04 2017 +0200
     7.3 @@ -273,7 +273,7 @@
     7.4                case Nil => Nil
     7.5                case sessions =>
     7.6                  HTML.break :::
     7.7 -                List(HTML.error_message(HTML.span(HTML.text("Failed sessions:")))) :::
     7.8 +                List(HTML.span(HTML.error_message, HTML.text("Failed sessions:"))) :::
     7.9                  List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
    7.10              })
    7.11            }))))))
    7.12 @@ -416,7 +416,7 @@
    7.13                HTML.text(" (" + session.head.timing.message_resources + ")"))))) ::
    7.14          data_entry.sessions.flatMap(session =>
    7.15            List(
    7.16 -            HTML.id("session_" + session.name)(HTML.section(session.name)),
    7.17 +            HTML.section(HTML.id("session_" + session.name), session.name),
    7.18              HTML.par(
    7.19                HTML.description(
    7.20                  List(
     8.1 --- a/src/Pure/General/graphics_file.scala	Thu Jun 01 16:56:05 2017 +0200
     8.2 +++ b/src/Pure/General/graphics_file.scala	Fri Jun 02 09:26:04 2017 +0200
     8.3 @@ -46,7 +46,7 @@
     8.4      val mapper = new DefaultFontMapper
     8.5      for {
     8.6        font <- Isabelle_System.fonts()
     8.7 -      name <- Library.try_unsuffix(".ttf", font.base.implode)
     8.8 +      name <- Library.try_unsuffix(".ttf", font.base_name)
     8.9      } {
    8.10        val parameters = new DefaultFontMapper.BaseFontParameters(File.platform_path(font))
    8.11        parameters.encoding = BaseFont.IDENTITY_H
     9.1 --- a/src/Pure/General/http.scala	Thu Jun 01 16:56:05 2017 +0200
     9.2 +++ b/src/Pure/General/http.scala	Fri Jun 02 09:26:04 2017 +0200
     9.3 @@ -137,7 +137,7 @@
     9.4  
     9.5    private lazy val html_fonts: SortedMap[String, Bytes] =
     9.6      SortedMap(
     9.7 -      Isabelle_System.fonts(html = true).map(path => (path.base.implode -> Bytes.read(path))): _*)
     9.8 +      Isabelle_System.fonts(html = true).map(path => (path.base_name -> Bytes.read(path))): _*)
     9.9  
    9.10    def fonts(root: String = "/fonts"): Handler =
    9.11      get(root, uri =>
    10.1 --- a/src/Pure/General/path.ML	Thu Jun 01 16:56:05 2017 +0200
    10.2 +++ b/src/Pure/General/path.ML	Fri Jun 02 09:26:04 2017 +0200
    10.3 @@ -29,6 +29,7 @@
    10.4    val print: T -> string
    10.5    val dir: T -> T
    10.6    val base: T -> T
    10.7 +  val base_name: T -> string
    10.8    val ext: string -> T -> T
    10.9    val split_ext: T -> T * string
   10.10    val expand: T -> T
   10.11 @@ -183,6 +184,7 @@
   10.12  
   10.13  val dir = split_path #1;
   10.14  val base = split_path (fn (_, s) => Path [Basic s]);
   10.15 +val base_name = implode_path o base;
   10.16  
   10.17  fun ext "" = I
   10.18    | ext e = split_path (fn (prfx, s) => append prfx (basic (s ^ "." ^ e)));
    11.1 --- a/src/Pure/General/path.scala	Thu Jun 01 16:56:05 2017 +0200
    11.2 +++ b/src/Pure/General/path.scala	Fri Jun 02 09:26:04 2017 +0200
    11.3 @@ -149,6 +149,7 @@
    11.4  
    11.5    def dir: Path = split_path._1
    11.6    def base: Path = new Path(List(Path.Basic(split_path._2)))
    11.7 +  def base_name: String = base.implode
    11.8  
    11.9    def ext(e: String): Path =
   11.10      if (e == "") this
    12.1 --- a/src/Pure/General/symbol.scala	Thu Jun 01 16:56:05 2017 +0200
    12.2 +++ b/src/Pure/General/symbol.scala	Fri Jun 02 09:26:04 2017 +0200
    12.3 @@ -487,10 +487,10 @@
    12.4      val sup_decoded = decode(sup)
    12.5      val bold_decoded = decode(bold)
    12.6      val emph_decoded = decode(emph)
    12.7 -    val bsub_decoded = decode("\\<^bsub>")
    12.8 -    val esub_decoded = decode("\\<^esub>")
    12.9 -    val bsup_decoded = decode("\\<^bsup>")
   12.10 -    val esup_decoded = decode("\\<^esup>")
   12.11 +    val bsub_decoded = decode(bsub)
   12.12 +    val esub_decoded = decode(esub)
   12.13 +    val bsup_decoded = decode(bsup)
   12.14 +    val esup_decoded = decode(esup)
   12.15    }
   12.16  
   12.17  
   12.18 @@ -585,6 +585,10 @@
   12.19    val sup = "\\<^sup>"
   12.20    val bold = "\\<^bold>"
   12.21    val emph = "\\<^emph>"
   12.22 +  val bsub = "\\<^bsub>"
   12.23 +  val esub = "\\<^esub>"
   12.24 +  val bsup = "\\<^bsup>"
   12.25 +  val esup = "\\<^esup>"
   12.26  
   12.27    def sub_decoded: Symbol = symbols.sub_decoded
   12.28    def sup_decoded: Symbol = symbols.sup_decoded
    13.1 --- a/src/Pure/PIDE/xml.scala	Thu Jun 01 16:56:05 2017 +0200
    13.2 +++ b/src/Pure/PIDE/xml.scala	Fri Jun 02 09:26:04 2017 +0200
    13.3 @@ -93,33 +93,44 @@
    13.4  
    13.5    /** string representation **/
    13.6  
    13.7 +  def output_char(c: Char, s: StringBuilder)
    13.8 +  {
    13.9 +    c match {
   13.10 +      case '<' => s ++= "&lt;"
   13.11 +      case '>' => s ++= "&gt;"
   13.12 +      case '&' => s ++= "&amp;"
   13.13 +      case '"' => s ++= "&quot;"
   13.14 +      case '\'' => s ++= "&apos;"
   13.15 +      case _ => s += c
   13.16 +    }
   13.17 +  }
   13.18 +
   13.19 +  def output_string(str: String, s: StringBuilder)
   13.20 +  {
   13.21 +    if (str == null) s ++= str
   13.22 +    else str.iterator.foreach(c => output_char(c, s))
   13.23 +  }
   13.24 +
   13.25    def string_of_body(body: Body): String =
   13.26    {
   13.27      val s = new StringBuilder
   13.28  
   13.29 -    def text(txt: String) {
   13.30 -      if (txt == null) s ++= txt
   13.31 -      else {
   13.32 -        for (c <- txt.iterator) c match {
   13.33 -          case '<' => s ++= "&lt;"
   13.34 -          case '>' => s ++= "&gt;"
   13.35 -          case '&' => s ++= "&amp;"
   13.36 -          case '"' => s ++= "&quot;"
   13.37 -          case '\'' => s ++= "&apos;"
   13.38 -          case _ => s += c
   13.39 -        }
   13.40 +    def text(txt: String) { output_string(txt, s) }
   13.41 +    def elem(markup: Markup)
   13.42 +    {
   13.43 +      s ++= markup.name
   13.44 +      for ((a, b) <- markup.properties) {
   13.45 +        s += ' '; s ++= a; s += '='; s += '"'; text(b); s += '"'
   13.46        }
   13.47      }
   13.48 -    def attrib(p: (String, String)) { s ++= " "; s ++= p._1; s ++= "=\""; text(p._2); s ++= "\"" }
   13.49 -    def elem(markup: Markup) { s ++= markup.name; markup.properties.foreach(attrib) }
   13.50      def tree(t: Tree): Unit =
   13.51        t match {
   13.52          case XML.Elem(markup, Nil) =>
   13.53 -          s ++= "<"; elem(markup); s ++= "/>"
   13.54 +          s += '<'; elem(markup); s ++= "/>"
   13.55          case XML.Elem(markup, ts) =>
   13.56 -          s ++= "<"; elem(markup); s ++= ">"
   13.57 +          s += '<'; elem(markup); s += '>'
   13.58            ts.foreach(tree)
   13.59 -          s ++= "</"; s ++= markup.name; s ++= ">"
   13.60 +          s ++= "</"; s ++= markup.name; s += '>'
   13.61          case XML.Text(txt) => text(txt)
   13.62        }
   13.63      body.foreach(tree)
    14.1 --- a/src/Pure/Thy/html.scala	Thu Jun 01 16:56:05 2017 +0200
    14.2 +++ b/src/Pure/Thy/html.scala	Fri Jun 02 09:26:04 2017 +0200
    14.3 @@ -9,51 +9,61 @@
    14.4  
    14.5  object HTML
    14.6  {
    14.7 -  /* encode text with control symbols */
    14.8 +  /* output text with control symbols */
    14.9  
   14.10 -  val control =
   14.11 +  private val control =
   14.12      Map(
   14.13 -      Symbol.sub -> "sub",
   14.14 -      Symbol.sub_decoded -> "sub",
   14.15 -      Symbol.sup -> "sup",
   14.16 -      Symbol.sup_decoded -> "sup",
   14.17 -      Symbol.bold -> "b",
   14.18 -      Symbol.bold_decoded -> "b")
   14.19 +      Symbol.sub -> "sub", Symbol.sub_decoded -> "sub",
   14.20 +      Symbol.sup -> "sup", Symbol.sup_decoded -> "sup",
   14.21 +      Symbol.bold -> "b", Symbol.bold_decoded -> "b")
   14.22 +
   14.23 +  private val control_block =
   14.24 +    Map(
   14.25 +      Symbol.bsub -> "<sub>", Symbol.bsub_decoded -> "<sub>",
   14.26 +      Symbol.esub -> "</sub>", Symbol.esub_decoded -> "</sub>",
   14.27 +      Symbol.bsup -> "<sup>", Symbol.bsup_decoded -> "<sup>",
   14.28 +      Symbol.esup -> "</sup>", Symbol.esup_decoded -> "</sup>")
   14.29 +
   14.30 +  def is_control(sym: Symbol.Symbol): Boolean = control.isDefinedAt(sym)
   14.31  
   14.32 -  def output(text: String, s: StringBuilder)
   14.33 +  def output(text: String, s: StringBuilder, hidden: Boolean)
   14.34    {
   14.35 -    def output_char(c: Char) =
   14.36 -      c match {
   14.37 -        case '<' => s ++= "&lt;"
   14.38 -        case '>' => s ++= "&gt;"
   14.39 -        case '&' => s ++= "&amp;"
   14.40 -        case '"' => s ++= "&quot;"
   14.41 -        case '\'' => s ++= "&#39;"
   14.42 -        case '\n' => s ++= "<br/>"
   14.43 -        case _ => s += c
   14.44 +    def output_hidden(body: => Unit): Unit =
   14.45 +      if (hidden) { s ++= "<span class=\"hidden\">"; body; s ++= "</span>" }
   14.46 +
   14.47 +    def output_symbol(sym: Symbol.Symbol): Unit =
   14.48 +      if (sym != "") {
   14.49 +        control_block.get(sym) match {
   14.50 +          case Some(html) if html.startsWith("</") =>
   14.51 +            s ++= html; output_hidden(XML.output_string(sym, s))
   14.52 +          case Some(html) =>
   14.53 +            output_hidden(XML.output_string(sym, s)); s ++= html
   14.54 +          case None =>
   14.55 +            XML.output_string(sym, s)
   14.56 +        }
   14.57        }
   14.58 -    def output_chars(str: String) = str.iterator.foreach(output_char(_))
   14.59  
   14.60      var ctrl = ""
   14.61      for (sym <- Symbol.iterator(text)) {
   14.62 -      if (control.isDefinedAt(sym)) ctrl = sym
   14.63 +      if (is_control(sym)) { output_symbol(ctrl); ctrl = sym }
   14.64        else {
   14.65          control.get(ctrl) match {
   14.66            case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
   14.67 -            s ++= ("<" + elem + ">")
   14.68 -            output_chars(sym)
   14.69 -            s ++= ("</" + elem + ">")
   14.70 +            output_hidden(output_symbol(ctrl))
   14.71 +            s += '<'; s ++= elem; s += '>'
   14.72 +            output_symbol(sym)
   14.73 +            s ++= "</"; s ++= elem; s += '>'
   14.74            case _ =>
   14.75 -            output_chars(ctrl)
   14.76 -            output_chars(sym)
   14.77 +            output_symbol(ctrl)
   14.78 +            output_symbol(sym)
   14.79          }
   14.80          ctrl = ""
   14.81        }
   14.82      }
   14.83 -    output_chars(ctrl)
   14.84 +    output_symbol(ctrl)
   14.85    }
   14.86  
   14.87 -  def output(text: String): String = Library.make_string(output(text, _))
   14.88 +  def output(text: String): String = Library.make_string(output(text, _, hidden = false))
   14.89  
   14.90  
   14.91    /* output XML as HTML */
   14.92 @@ -62,41 +72,51 @@
   14.93      Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
   14.94        "ul", "ol", "dl", "li", "dt", "dd")
   14.95  
   14.96 -  def output(body: XML.Body, s: StringBuilder)
   14.97 +  def output(body: XML.Body, s: StringBuilder, hidden: Boolean)
   14.98    {
   14.99 -    def attrib(p: (String, String)): Unit =
  14.100 -      { s ++= " "; s ++= p._1; s ++= "=\""; output(p._2, s); s ++= "\"" }
  14.101 -    def elem(markup: Markup): Unit =
  14.102 -      { s ++= markup.name; markup.properties.foreach(attrib) }
  14.103 +    def elem(markup: Markup)
  14.104 +    {
  14.105 +      s ++= markup.name
  14.106 +      for ((a, b) <- markup.properties) {
  14.107 +        s += ' '; s ++= a; s += '='; s += '"'; output(b, s, hidden); s += '"'
  14.108 +      }
  14.109 +    }
  14.110      def tree(t: XML.Tree): Unit =
  14.111        t match {
  14.112          case XML.Elem(markup, Nil) =>
  14.113 -          s ++= "<"; elem(markup); s ++= "/>"
  14.114 +          s += '<'; elem(markup); s ++= "/>"
  14.115          case XML.Elem(markup, ts) =>
  14.116            if (structural_elements(markup.name)) s += '\n'
  14.117 -          s ++= "<"; elem(markup); s ++= ">"
  14.118 +          s += '<'; elem(markup); s += '>'
  14.119            ts.foreach(tree)
  14.120 -          s ++= "</"; s ++= markup.name; s ++= ">"
  14.121 +          s ++= "</"; s ++= markup.name; s += '>'
  14.122            if (structural_elements(markup.name)) s += '\n'
  14.123 -        case XML.Text(txt) => output(txt, s)
  14.124 +        case XML.Text(txt) =>
  14.125 +          output(txt, s, hidden)
  14.126        }
  14.127      body.foreach(tree)
  14.128    }
  14.129  
  14.130 -  def output(body: XML.Body): String = Library.make_string(output(body, _))
  14.131 -  def output(tree: XML.Tree): String = output(List(tree))
  14.132 +  def output(body: XML.Body, hidden: Boolean): String =
  14.133 +    Library.make_string(output(body, _, hidden))
  14.134 +
  14.135 +  def output(tree: XML.Tree, hidden: Boolean): String =
  14.136 +    output(List(tree), hidden)
  14.137  
  14.138  
  14.139    /* attributes */
  14.140  
  14.141 -  class Attribute(name: String, value: String)
  14.142 -  { def apply(elem: XML.Elem): XML.Elem = elem + (name -> value) }
  14.143 +  class Attribute(val name: String, value: String)
  14.144 +  {
  14.145 +    def xml: XML.Attribute = name -> value
  14.146 +    def apply(elem: XML.Elem): XML.Elem = elem + xml
  14.147 +  }
  14.148  
  14.149 -  def id(s: String) = new Attribute("id", s)
  14.150 -  def css_class(name: String) = new Attribute("class", name)
  14.151 +  def id(s: String): Attribute = new Attribute("id", s)
  14.152 +  def class_(name: String): Attribute = new Attribute("class", name)
  14.153  
  14.154 -  def width(w: Int) = new Attribute("width", w.toString)
  14.155 -  def height(h: Int) = new Attribute("height", h.toString)
  14.156 +  def width(w: Int): Attribute = new Attribute("width", w.toString)
  14.157 +  def height(h: Int): Attribute = new Attribute("height", h.toString)
  14.158    def size(w: Int, h: Int)(elem: XML.Elem): XML.Elem = width(w)(height(h)(elem))
  14.159  
  14.160  
  14.161 @@ -105,11 +125,19 @@
  14.162    def text(txt: String): XML.Body = if (txt.isEmpty) Nil else List(XML.Text(txt))
  14.163    val break: XML.Body = List(XML.elem("br"))
  14.164  
  14.165 -  class Operator(name: String)
  14.166 -  { def apply(body: XML.Body): XML.Elem = XML.elem(name, body) }
  14.167 +  class Operator(val name: String)
  14.168 +  {
  14.169 +    def apply(body: XML.Body): XML.Elem = XML.elem(name, body)
  14.170 +    def apply(att: Attribute, body: XML.Body): XML.Elem = att(apply(body))
  14.171 +    def apply(c: String, body: XML.Body): XML.Elem = apply(class_(c), body)
  14.172 +  }
  14.173  
  14.174    class Heading(name: String) extends Operator(name)
  14.175 -  { def apply(txt: String): XML.Elem = super.apply(text(txt)) }
  14.176 +  {
  14.177 +    def apply(txt: String): XML.Elem = super.apply(text(txt))
  14.178 +    def apply(att: Attribute, txt: String): XML.Elem = super.apply(att, text(txt))
  14.179 +    def apply(c: String, txt: String): XML.Elem = super.apply(c, text(txt))
  14.180 +  }
  14.181  
  14.182    val div = new Operator("div")
  14.183    val span = new Operator("span")
  14.184 @@ -142,28 +170,31 @@
  14.185    def image(src: String, alt: String = ""): XML.Elem =
  14.186      XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
  14.187  
  14.188 -  def source(src: String): XML.Elem = css_class("source")(div(List(pre(text(src)))))
  14.189 +  def source(src: String): XML.Elem = pre("source", text(src))
  14.190  
  14.191    def style(s: String): XML.Elem = XML.elem("style", text(s))
  14.192  
  14.193 +  def style_file(href: String): XML.Elem =
  14.194 +    XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
  14.195 +
  14.196  
  14.197    /* messages */
  14.198  
  14.199    // background
  14.200 -  val writeln_message: Attribute = css_class("writeln_message")
  14.201 -  val warning_message: Attribute = css_class("warning_message")
  14.202 -  val error_message: Attribute = css_class("error_message")
  14.203 +  val writeln_message: Attribute = class_("writeln_message")
  14.204 +  val warning_message: Attribute = class_("warning_message")
  14.205 +  val error_message: Attribute = class_("error_message")
  14.206  
  14.207    // underline
  14.208 -  val writeln: Attribute = css_class("writeln")
  14.209 -  val warning: Attribute = css_class("warning")
  14.210 -  val error: Attribute = css_class("error")
  14.211 +  val writeln: Attribute = class_("writeln")
  14.212 +  val warning: Attribute = class_("warning")
  14.213 +  val error: Attribute = class_("error")
  14.214  
  14.215  
  14.216    /* tooltips */
  14.217  
  14.218    def tooltip(item: XML.Body, tip: XML.Body): XML.Elem =
  14.219 -    span(item ::: List(css_class("tooltip")(div(tip))))
  14.220 +    span(item ::: List(div("tooltip", tip)))
  14.221  
  14.222    def tooltip_errors(item: XML.Body, msgs: List[XML.Body]): XML.Elem =
  14.223      HTML.error(tooltip(item, msgs.map(msg => error_message(pre(msg)))))
  14.224 @@ -180,28 +211,66 @@
  14.225      XML.Elem(Markup("meta",
  14.226        List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil)
  14.227  
  14.228 -  def head_css(css: String): XML.Elem =
  14.229 -    XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> css)), Nil)
  14.230 -
  14.231 -  def output_document(head: XML.Body, body: XML.Body, css: String = "isabelle.css"): String =
  14.232 +  def output_document(head: XML.Body, body: XML.Body,
  14.233 +    css: String = "isabelle.css", hidden: Boolean = true): String =
  14.234 +  {
  14.235      cat_lines(
  14.236        List(header,
  14.237 -        output(XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head)),
  14.238 -        output(XML.elem("body", body))))
  14.239 +        output(
  14.240 +          XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head),
  14.241 +          hidden = hidden),
  14.242 +        output(XML.elem("body", body), hidden = hidden)))
  14.243 +  }
  14.244 +
  14.245 +
  14.246 +  /* fonts */
  14.247 +
  14.248 +  def fonts_url(): String => String =
  14.249 +    (for (font <- Isabelle_System.fonts(html = true))
  14.250 +     yield (font.base_name -> Url.print_file(font.file))).toMap
  14.251 +
  14.252 +  def fonts_dir(prefix: String)(ttf_name: String): String =
  14.253 +    prefix + "/" + ttf_name
  14.254 +
  14.255 +  def fonts_css(make_url: String => String = fonts_url()): String =
  14.256 +  {
  14.257 +    def font_face(name: String, ttf_name: String, bold: Boolean = false): String =
  14.258 +      cat_lines(
  14.259 +        List(
  14.260 +          "@font-face {",
  14.261 +          "  font-family: '" + name + "';",
  14.262 +          "  src: url('" + make_url(ttf_name) + "') format('truetype');") :::
  14.263 +        (if (bold) List("  font-weight: bold;") else Nil) :::
  14.264 +        List("}"))
  14.265 +
  14.266 +    List(
  14.267 +      "/* Isabelle fonts */",
  14.268 +      font_face("IsabelleText", "IsabelleText.ttf"),
  14.269 +      font_face("IsabelleText", "IsabelleTextBold.ttf", bold = true),
  14.270 +      font_face("Vacuous", "Vacuous.ttf")).mkString("\n\n")
  14.271 +  }
  14.272  
  14.273  
  14.274    /* document directory */
  14.275  
  14.276 +  def isabelle_css: Path = Path.explode("~~/etc/isabelle.css")
  14.277 +
  14.278 +  def write_isabelle_css(dir: Path, make_url: String => String = fonts_dir("fonts"))
  14.279 +  {
  14.280 +    File.write(dir + isabelle_css.base,
  14.281 +      fonts_css(make_url) + "\n\n\n" + File.read(isabelle_css))
  14.282 +  }
  14.283 +
  14.284    def init_dir(dir: Path)
  14.285    {
  14.286      Isabelle_System.mkdirs(dir)
  14.287 -    File.copy(Path.explode("~~/etc/isabelle.css"), dir)
  14.288 +    write_isabelle_css(dir)
  14.289    }
  14.290  
  14.291    def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
  14.292 -    css: String = "isabelle.css")
  14.293 +    css: String = isabelle_css.base_name, hidden: Boolean = true)
  14.294    {
  14.295      init_dir(dir)
  14.296 -    File.write(dir + Path.basic(name), output_document(head, body, css))
  14.297 +    File.write(dir + Path.basic(name), output_document(head, body, css = css, hidden = hidden))
  14.298    }
  14.299  }
    15.1 --- a/src/Pure/Thy/present.scala	Thu Jun 01 16:56:05 2017 +0200
    15.2 +++ b/src/Pure/Thy/present.scala	Fri Jun 02 09:26:04 2017 +0200
    15.3 @@ -52,12 +52,12 @@
    15.4        HTML.chapter(title) ::
    15.5         (if (sessions.isEmpty) Nil
    15.6          else
    15.7 -          List(HTML.css_class("sessions")(HTML.div(List(
    15.8 -            HTML.description(
    15.9 +          List(HTML.div("sessions",
   15.10 +            List(HTML.description(
   15.11                sessions.map({ case (name, description) =>
   15.12                  (List(HTML.link(name + "/index.html", HTML.text(name))),
   15.13                    if (description == "") Nil
   15.14 -                  else List(HTML.pre(HTML.text(description)))) }))))))))
   15.15 +                  else List(HTML.pre(HTML.text(description)))) })))))))
   15.16    }
   15.17  
   15.18    def make_global_index(browser_info: Path)
   15.19 @@ -93,7 +93,7 @@
   15.20        File.copy(graph_file, session_graph.file)
   15.21        Isabelle_System.bash("chmod a+r " + File.bash_path(session_graph))
   15.22  
   15.23 -      File.copy(Path.explode("~~/etc/isabelle.css"), session_prefix)
   15.24 +      HTML.write_isabelle_css(session_prefix)
   15.25  
   15.26        for (font <- Isabelle_System.fonts(html = true))
   15.27          File.copy(font, session_fonts)
    16.1 --- a/src/Pure/Thy/sessions.scala	Thu Jun 01 16:56:05 2017 +0200
    16.2 +++ b/src/Pure/Thy/sessions.scala	Fri Jun 02 09:26:04 2017 +0200
    16.3 @@ -574,7 +574,7 @@
    16.4            val global_theories =
    16.5              for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global }
    16.6              yield {
    16.7 -              val thy_name = Path.explode(thy).expand.base.implode
    16.8 +              val thy_name = Path.explode(thy).expand.base_name
    16.9                if (Long_Name.is_qualified(thy_name))
   16.10                  error("Bad qualified name for global theory " +
   16.11                    quote(thy_name) + Position.here(pos))
    17.1 --- a/src/Pure/Thy/thy_header.ML	Thu Jun 01 16:56:05 2017 +0200
    17.2 +++ b/src/Pure/Thy/thy_header.ML	Fri Jun 02 09:26:04 2017 +0200
    17.3 @@ -114,7 +114,7 @@
    17.4  val ml_roots = ["ML_Root0", "ML_Root"];
    17.5  val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"];
    17.6  
    17.7 -val import_name = Path.implode o Path.base o Path.explode;
    17.8 +val import_name = Path.base_name o Path.explode;
    17.9  
   17.10  
   17.11  (* header args *)
    18.1 --- a/src/Pure/Tools/spell_checker.scala	Thu Jun 01 16:56:05 2017 +0200
    18.2 +++ b/src/Pure/Tools/spell_checker.scala	Fri Jun 02 09:26:04 2017 +0200
    18.3 @@ -57,7 +57,7 @@
    18.4  
    18.5    class Dictionary private[Spell_Checker](val path: Path)
    18.6    {
    18.7 -    val lang = path.split_ext._1.base.implode
    18.8 +    val lang = path.split_ext._1.base_name
    18.9      val user_path = Path.explode("$ISABELLE_HOME_USER/dictionaries") + Path.basic(lang)
   18.10      override def toString: String = lang
   18.11    }
    19.1 --- a/src/Tools/VSCode/extension/package.json	Thu Jun 01 16:56:05 2017 +0200
    19.2 +++ b/src/Tools/VSCode/extension/package.json	Fri Jun 02 09:26:04 2017 +0200
    19.3 @@ -10,7 +10,7 @@
    19.4          "document preparation"
    19.5          ],
    19.6      "icon": "isabelle.png",
    19.7 -    "version": "0.12.0",
    19.8 +    "version": "0.13.0",
    19.9      "publisher": "makarius",
   19.10      "license": "MIT",
   19.11      "repository": { "url": "http://isabelle.in.tum.de/repos/isabelle" },
    20.1 --- a/src/Tools/VSCode/extension/src/preview.ts	Thu Jun 01 16:56:05 2017 +0200
    20.2 +++ b/src/Tools/VSCode/extension/src/preview.ts	Fri Jun 02 09:26:04 2017 +0200
    20.3 @@ -79,8 +79,10 @@
    20.4        const preview_uri = encode_preview(Uri.parse(params.uri))
    20.5        if (preview_uri) {
    20.6          preview_content.set(preview_uri.toString(), params.content)
    20.7 -        if (params.column == 0) content_provider.update(preview_uri)
    20.8 -        else commands.executeCommand("vscode.previewHtml", preview_uri, params.column, params.label)
    20.9 +        content_provider.update(preview_uri)
   20.10 +        if (params.column != 0) {
   20.11 +          commands.executeCommand("vscode.previewHtml", preview_uri, params.column, params.label)
   20.12 +        }
   20.13        }
   20.14      })
   20.15  }
    21.1 --- a/src/Tools/VSCode/src/preview.scala	Thu Jun 01 16:56:05 2017 +0200
    21.2 +++ b/src/Tools/VSCode/src/preview.scala	Fri Jun 02 09:26:04 2017 +0200
    21.3 @@ -45,14 +45,12 @@
    21.4    {
    21.5      val label = "Preview " + quote(model.node_name.toString)
    21.6      val content =
    21.7 -      HTML.output_document(head = Nil, css = "", body =
    21.8 +      HTML.output_document(
    21.9 +        List(HTML.style(HTML.fonts_css()), HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
   21.10          List(
   21.11 -          HTML.chapter(label),
   21.12 -          HTML.itemize(
   21.13 -            snapshot.node.commands.toList.flatMap(
   21.14 -              command =>
   21.15 -                if (command.span.name == "") None
   21.16 -                else Some(HTML.text(command.span.name))))))
   21.17 +          HTML.chapter("Theory " + quote(model.node_name.theory_base_name)),
   21.18 +          HTML.source(Symbol.decode(snapshot.node.commands.iterator.map(_.source).mkString))),
   21.19 +        css = "")
   21.20      (label, content)
   21.21    }
   21.22  }
    22.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Jun 01 16:56:05 2017 +0200
    22.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Fri Jun 02 09:26:04 2017 +0200
    22.3 @@ -193,7 +193,7 @@
    22.4            val path = Path.explode(text)
    22.5            val (dir, base_name) =
    22.6              if (text == "" || text.endsWith("/")) (path, "")
    22.7 -            else (path.dir, path.base.implode)
    22.8 +            else (path.dir, path.base_name)
    22.9  
   22.10            val directory = new JFile(PIDE.resources.append(rendering.snapshot.node_name, dir))
   22.11            val files = directory.listFiles
    23.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Thu Jun 01 16:56:05 2017 +0200
    23.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Fri Jun 02 09:26:04 2017 +0200
    23.3 @@ -96,7 +96,7 @@
    23.4      action =
    23.5        Action(Symbol.decode(symbol)) {
    23.6          val text_area = view.getTextArea
    23.7 -        if (is_control && HTML.control.isDefinedAt(symbol))
    23.8 +        if (is_control && HTML.is_control(symbol))
    23.9            Syntax_Style.edit_control_style(text_area, symbol)
   23.10          else
   23.11            text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol))
    24.1 --- a/src/Tools/jEdit/src/syntax_style.scala	Thu Jun 01 16:56:05 2017 +0200
    24.2 +++ b/src/Tools/jEdit/src/syntax_style.scala	Fri Jun 02 09:26:04 2017 +0200
    24.3 @@ -138,7 +138,7 @@
    24.4      def update_style(text: String): String =
    24.5      {
    24.6        val result = new StringBuilder
    24.7 -      for (sym <- Symbol.iterator(text) if !HTML.control.isDefinedAt(sym)) {
    24.8 +      for (sym <- Symbol.iterator(text) if !HTML.is_control(sym)) {
    24.9          if (Symbol.is_controllable(sym)) result ++= control_decoded
   24.10          result ++= sym
   24.11        }
   24.12 @@ -148,7 +148,7 @@
   24.13      text_area.getSelection.foreach(sel => {
   24.14        val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
   24.15        JEdit_Lib.try_get_text(buffer, before) match {
   24.16 -        case Some(s) if HTML.control.isDefinedAt(s) =>
   24.17 +        case Some(s) if HTML.is_control(s) =>
   24.18            text_area.extendSelection(before.start, before.stop)
   24.19          case _ =>
   24.20        }