more tight HTML output: avoid extra lines within <pre>;
authorwenzelm
Wed Jan 03 22:29:31 2018 +0100 (2 weeks ago)
changeset 673374254cfd15b00
parent 67336 3ee6da378183
child 67338 b164fdbb423d
more tight HTML output: avoid extra lines within <pre>;
src/Pure/Thy/html.scala
src/Pure/Thy/present.scala
src/Tools/VSCode/src/state_panel.scala
     1.1 --- a/src/Pure/Thy/html.scala	Wed Jan 03 20:55:13 2018 +0100
     1.2 +++ b/src/Pure/Thy/html.scala	Wed Jan 03 22:29:31 2018 +0100
     1.3 @@ -97,7 +97,7 @@
     1.4      Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
     1.5        "ul", "ol", "dl", "li", "dt", "dd")
     1.6  
     1.7 -  def output(body: XML.Body, s: StringBuilder, hidden: Boolean)
     1.8 +  def output(body: XML.Body, s: StringBuilder, hidden: Boolean, structural: Boolean)
     1.9    {
    1.10      def elem(markup: Markup)
    1.11      {
    1.12 @@ -116,22 +116,22 @@
    1.13          case XML.Elem(markup, Nil) =>
    1.14            s += '<'; elem(markup); s ++= "/>"
    1.15          case XML.Elem(markup, ts) =>
    1.16 -          if (structural_elements(markup.name)) s += '\n'
    1.17 +          if (structural && structural_elements(markup.name)) s += '\n'
    1.18            s += '<'; elem(markup); s += '>'
    1.19            ts.foreach(tree)
    1.20            s ++= "</"; s ++= markup.name; s += '>'
    1.21 -          if (structural_elements(markup.name)) s += '\n'
    1.22 +          if (structural && structural_elements(markup.name)) s += '\n'
    1.23          case XML.Text(txt) =>
    1.24            output(txt, s, hidden = hidden, permissive = true)
    1.25        }
    1.26      body.foreach(tree)
    1.27    }
    1.28  
    1.29 -  def output(body: XML.Body, hidden: Boolean): String =
    1.30 -    Library.make_string(output(body, _, hidden))
    1.31 +  def output(body: XML.Body, hidden: Boolean, structural: Boolean): String =
    1.32 +    Library.make_string(output(body, _, hidden, structural))
    1.33  
    1.34 -  def output(tree: XML.Tree, hidden: Boolean): String =
    1.35 -    output(List(tree), hidden)
    1.36 +  def output(tree: XML.Tree, hidden: Boolean, structural: Boolean): String =
    1.37 +    output(List(tree), hidden, structural)
    1.38  
    1.39  
    1.40    /* attributes */
    1.41 @@ -333,14 +333,17 @@
    1.42        List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil)
    1.43  
    1.44    def output_document(head: XML.Body, body: XML.Body,
    1.45 -    css: String = "isabelle.css", hidden: Boolean = true): String =
    1.46 +    css: String = "isabelle.css",
    1.47 +    hidden: Boolean = true,
    1.48 +    structural: Boolean = true): String =
    1.49    {
    1.50      cat_lines(
    1.51        List(header,
    1.52          output(
    1.53            XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head),
    1.54 -          hidden = hidden),
    1.55 -        output(XML.elem("body", body), hidden = hidden)))
    1.56 +          hidden = hidden, structural = structural),
    1.57 +        output(XML.elem("body", body),
    1.58 +          hidden = hidden, structural = structural)))
    1.59    }
    1.60  
    1.61  
    1.62 @@ -389,9 +392,12 @@
    1.63    }
    1.64  
    1.65    def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
    1.66 -    css: String = isabelle_css.base_name, hidden: Boolean = true)
    1.67 +    css: String = isabelle_css.base_name,
    1.68 +    hidden: Boolean = true,
    1.69 +    structural: Boolean = true)
    1.70    {
    1.71      init_dir(dir)
    1.72 -    File.write(dir + Path.basic(name), output_document(head, body, css = css, hidden = hidden))
    1.73 +    File.write(dir + Path.basic(name),
    1.74 +      output_document(head, body, css = css, hidden = hidden, structural = structural))
    1.75    }
    1.76  }
     2.1 --- a/src/Pure/Thy/present.scala	Wed Jan 03 20:55:13 2018 +0100
     2.2 +++ b/src/Pure/Thy/present.scala	Wed Jan 03 22:29:31 2018 +0100
     2.3 @@ -116,7 +116,7 @@
     2.4          List(
     2.5            HTML.style(HTML.fonts_css(fonts_url) + File.read(HTML.isabelle_css)),
     2.6            HTML.title(title)),
     2.7 -        List(HTML.source(body)), css = "")
     2.8 +        List(HTML.source(body)), css = "", structural = false)
     2.9  
    2.10      val name = snapshot.node_name
    2.11      if (plain_text) {
    2.12 @@ -160,7 +160,9 @@
    2.13      }
    2.14  
    2.15    private def html_class(c: String, html: XML.Body): XML.Tree =
    2.16 -    if (html_div(html)) HTML.div(c, html) else HTML.span(c, html)
    2.17 +    if (html.forall(_ == HTML.no_text)) HTML.no_text
    2.18 +    else if (html_div(html)) HTML.div(c, html)
    2.19 +    else HTML.span(c, html)
    2.20  
    2.21    private def make_html(xml: XML.Body): XML.Body =
    2.22      xml map {
     3.1 --- a/src/Tools/VSCode/src/state_panel.scala	Wed Jan 03 20:55:13 2018 +0100
     3.2 +++ b/src/Tools/VSCode/src/state_panel.scala	Wed Jan 03 22:29:31 2018 +0100
     3.3 @@ -70,7 +70,7 @@
     3.4                  HTML.style_file(HTML.isabelle_css),
     3.5                  HTML.script(controls_script)),
     3.6                List(controls, HTML.source(text)),
     3.7 -              css = "")
     3.8 +              css = "", structural = true)
     3.9            output(content)
    3.10          })
    3.11