<commit_before>/*  Title:      Pure/Thy/html.scala
    Author:     Makarius

Basic HTML output.
*/

package isabelle

import scala.collection.mutable.ListBuffer


object HTML
{
  // common elements and attributes

  val BODY = "body"
  val DIV = "div"
  val SPAN = "span"
  val BR = "br"
  val PRE = "pre"
  val CLASS = "class"


  // document markup

  def span(cls: String, body: List[XML.Tree]): XML.Elem =
    XML.Elem(SPAN, List((CLASS, cls)), body)

  def hidden(txt: String): XML.Elem =
    span(Markup.HIDDEN, List(XML.Text(txt)))

  def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
  def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))

  def spans(tree: XML.Tree): List[XML.Tree] =
    tree match {
      case XML.Elem(name, _, ts) =>
        List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans)))))
      case XML.Text(txt) =>
        val ts = new ListBuffer[XML.Tree]
        val t = new StringBuilder
        def flush() {
          if (!t.isEmpty) {
            ts += XML.Text(t.toString)<commit_msg>added HTML.encode (in Scala), similar to HTML.output in ML;<commit_after>/*  Title:      Pure/Thy/html.scala
    Author:     Makarius

Basic HTML output.
*/

package isabelle

import scala.collection.mutable.ListBuffer


object HTML
{
  // encode text

  def encode(text: String): String =
  {
    val s = new StringBuilder
    for (c <- text.iterator) c match {
      case '<' => s ++= "&lt;"
      case '>' => s ++= "&gt;"
      case '&' => s ++= "&amp;"
      case '"' => s ++= "&quot;"
      case '\'' => s ++= "&#39;"
      case '\n' => s ++= "<br/>"
      case _ => s += c
    }
    s.toString
  }


  // common elements and attributes

  val BODY = "body"
  val DIV = "div"
  val SPAN = "span"
  val BR = "br"
  val PRE = "pre"
  val CLASS = "class"


  // document markup

  def span(cls: String, body: List[XML.Tree]): XML.Elem =
    XML.Elem(SPAN, List((CLASS, cls)), body)

  def hidden(txt: String): XML.Elem =
    span(Markup.HIDDEN, List(XML.Text(txt)))

  def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
  def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))

  def spans(tree: XML.Tree): List[XML.Tree] =
    tree match {
      case XML.Elem(name, _, ts) =>
        List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans)))))
      case XML.Text(txt) =>
        val ts = new ListBuffer[XML.Tree]
        val t = new StringBuilder
        def flush() {
          if (!t.isEmpty) {
            ts += XML.Text(t.toString)
{'fraction_non_alphanumeric': 0.17052136417091338, 'fraction_numerical': 0.0007840062720501764, 'mean_word_length': 2.5346260387811634, 'pattern_counts': {'":': 0, '<': 6, '<?xml version=': 0, '>': 16, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1425060', 'n_tokens_mistral': 934, 'n_tokens_neox': 899, 'n_words': 235}