src/Pure/Thy/html.scala
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 59063 b3c45d0e4fe1
child 60033 9a1d40876e9f
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
     1 /*  Title:      Pure/Thy/html.scala
     2     Module:     PIDE
     3     Author:     Makarius
     4 
     5 HTML presentation elements.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 object HTML
    12 {
    13   /* encode text with control symbols */
    14 
    15   val control_decoded =
    16     Map(Symbol.sub_decoded -> "sub",
    17       Symbol.sup_decoded -> "sup",
    18       Symbol.bold_decoded -> "b")
    19 
    20   def encode(text: String): String =
    21   {
    22     val result = new StringBuilder
    23 
    24     def encode_char(c: Char) =
    25       c match {
    26         case '<' => result ++= "&lt;"
    27         case '>' => result ++= "&gt;"
    28         case '&' => result ++= "&amp;"
    29         case '"' => result ++= "&quot;"
    30         case '\'' => result ++= "&#39;"
    31         case '\n' => result ++= "<br/>"
    32         case c => result += c
    33       }
    34     def encode_chars(s: String) = s.iterator.foreach(encode_char(_))
    35 
    36     var control = ""
    37     for (sym <- Symbol.iterator(text)) {
    38       if (control_decoded.isDefinedAt(sym)) control = sym
    39       else {
    40         control_decoded.get(control) match {
    41           case Some(elem) if Symbol.is_controllable(sym) && sym != "\"" =>
    42             result ++= ("<" + elem + ">")
    43             encode_chars(sym)
    44             result ++= ("</" + elem + ">")
    45           case _ =>
    46             encode_chars(control)
    47             encode_chars(sym)
    48         }
    49         control = ""
    50       }
    51     }
    52     encode_chars(control)
    53 
    54     result.toString
    55   }
    56 
    57 
    58   /* document */
    59 
    60   val end_document = "\n</div>\n</body>\n</html>\n"
    61 
    62   def begin_document(title: String): String =
    63     "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" +
    64     "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " +
    65     "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" +
    66     "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" +
    67     "<head>\n" +
    68     "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" +
    69     "<title>" + encode(title) + "</title>\n" +
    70     "<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" +
    71     "</head>\n" +
    72     "\n" +
    73     "<body>\n" +
    74     "<div class=\"head\">" +
    75     "<h1>" + encode(title) + "</h1>\n"
    76 
    77 
    78   /* common markup elements */
    79 
    80   private def session_entry(entry: (String, String)): String =
    81   {
    82     val (name, description) = entry
    83     val descr =
    84       if (description == "") Nil
    85       else List(XML.elem("br"), XML.elem("pre", List(XML.Text(description))))
    86     XML.string_of_tree(
    87       XML.elem("li",
    88         List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
    89           List(XML.Text(name)))) ::: descr)) + "\n"
    90   }
    91 
    92   def chapter_index(chapter: String, sessions: List[(String, String)]): String =
    93   {
    94     begin_document("Isabelle/" + chapter + " sessions") +
    95       (if (sessions.isEmpty) ""
    96        else "<div class=\"sessions\"><ul>\n" + sessions.map(session_entry(_)).mkString + "</ul>") +
    97     end_document
    98   }
    99 }