1.1 --- a/src/Pure/System/session.ML Thu Jan 03 17:40:36 2013 +0100
1.2 +++ b/src/Pure/System/session.ML Thu Jan 03 21:23:14 2013 +0100
1.3 @@ -8,6 +8,7 @@
1.4 sig
1.5 val id: unit -> string list
1.6 val name: unit -> string
1.7 + val path: unit -> string list
1.8 val welcome: unit -> string
1.9 val finish: unit -> unit
1.10 val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
2.1 --- a/src/Pure/Thy/html.scala Thu Jan 03 17:40:36 2013 +0100
2.2 +++ b/src/Pure/Thy/html.scala Thu Jan 03 21:23:14 2013 +0100
2.3 @@ -1,7 +1,7 @@
2.4 /* Title: Pure/Thy/html.scala
2.5 Author: Makarius
2.6
2.7 -Basic HTML output.
2.8 +HTML presentation elements.
2.9 */
2.10
2.11 package isabelle
2.12 @@ -29,75 +29,19 @@
2.13 }
2.14
2.15
2.16 - /// FIXME unused stuff
2.17 + // common markup elements
2.18
2.19 - // common elements and attributes
2.20 + def session_entry(name: String): String =
2.21 + XML.string_of_tree(
2.22 + XML.elem("li",
2.23 + List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
2.24 + List(XML.Text(name)))))) + "\n"
2.25
2.26 - val BODY = "body"
2.27 - val DIV = "div"
2.28 - val SPAN = "span"
2.29 - val BR = "br"
2.30 - val PRE = "pre"
2.31 - val CLASS = "class"
2.32 - val STYLE = "style"
2.33 + def session_entries(names: List[String]): String =
2.34 + if (names.isEmpty) "</ul>"
2.35 + else
2.36 + "</ul>\n</div>\n<div class=\"sessions\">\n" +
2.37 + "<h2>Sessions</h2>\n<ul>\n" + names.map(session_entry).mkString + "</ul>";
2.38
2.39 -
2.40 - // document markup
2.41 -
2.42 - def span(cls: String, body: XML.Body): XML.Elem =
2.43 - XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
2.44 -
2.45 - def user_font(font: String, txt: String): XML.Elem =
2.46 - XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
2.47 -
2.48 - def hidden(txt: String): XML.Elem =
2.49 - span(Markup.HIDDEN, List(XML.Text(txt)))
2.50 -
2.51 - def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
2.52 - def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
2.53 - def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
2.54 -
2.55 - def spans(input: XML.Tree): XML.Body =
2.56 - {
2.57 - def html_spans(tree: XML.Tree): XML.Body =
2.58 - tree match {
2.59 - case XML.Wrapped_Elem(markup, _, ts) =>
2.60 - List(span(markup.name, ts.flatMap(html_spans)))
2.61 - case XML.Elem(markup, ts) =>
2.62 - List(span(markup.name, ts.flatMap(html_spans)))
2.63 - case XML.Text(txt) =>
2.64 - val ts = new ListBuffer[XML.Tree]
2.65 - val t = new StringBuilder
2.66 - def flush() {
2.67 - if (!t.isEmpty) {
2.68 - ts += XML.Text(t.toString)
2.69 - t.clear
2.70 - }
2.71 - }
2.72 - def add(elem: XML.Tree) {
2.73 - flush()
2.74 - ts += elem
2.75 - }
2.76 - val syms = Symbol.iterator(txt)
2.77 - while (syms.hasNext) {
2.78 - val s1 = syms.next
2.79 - def s2() = if (syms.hasNext) syms.next else ""
2.80 - if (s1 == "\n") add(XML.elem(BR))
2.81 - else if (s1 == Symbol.sub_decoded || s1 == Symbol.isub_decoded)
2.82 - { add(hidden(s1)); add(sub(s2())) }
2.83 - else if (s1 == Symbol.sup_decoded || s1 == Symbol.isup_decoded)
2.84 - { add(hidden(s1)); add(sup(s2())) }
2.85 - else if (s1 == Symbol.bsub_decoded) t ++= s1 // FIXME
2.86 - else if (s1 == Symbol.esub_decoded) t ++= s1 // FIXME
2.87 - else if (s1 == Symbol.bsup_decoded) t ++= s1 // FIXME
2.88 - else if (s1 == Symbol.esup_decoded) t ++= s1 // FIXME
2.89 - else if (s1 == Symbol.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
2.90 - else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }
2.91 - else t ++= s1
2.92 - }
2.93 - flush()
2.94 - ts.toList
2.95 - }
2.96 - html_spans(input)
2.97 - }
2.98 + val end_document = "\n</div>\n</body>\n</html>\n"
2.99 }
3.1 --- a/src/Pure/Thy/present.ML Thu Jan 03 17:40:36 2013 +0100
3.2 +++ b/src/Pure/Thy/present.ML Thu Jan 03 21:23:14 2013 +0100
3.3 @@ -213,7 +213,7 @@
3.4
3.5 (** document preparation **)
3.6
3.7 -(* maintain index *)
3.8 +(* maintain session index *)
3.9
3.10 val session_entries =
3.11 HTML.session_entries o
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Pure/Thy/present.scala Thu Jan 03 21:23:14 2013 +0100
4.3 @@ -0,0 +1,41 @@
4.4 +/* Title: Pure/Thy/present.scala
4.5 + Author: Makarius
4.6 +
4.7 +Theory presentation: HTML.
4.8 +*/
4.9 +
4.10 +package isabelle
4.11 +
4.12 +
4.13 +object Present
4.14 +{
4.15 + /* maintain session index -- NOT thread-safe */
4.16 +
4.17 + private val index_path = Path.basic("index.html")
4.18 + private val session_entries_path = Path.explode(".session/entries")
4.19 + private val pre_index_path = Path.explode(".session/pre-index")
4.20 +
4.21 + private def get_entries(dir: Path): List[String] =
4.22 + split_lines(File.read(dir + session_entries_path))
4.23 +
4.24 + private def put_entries(entries: List[String], dir: Path): Unit =
4.25 + File.write(dir + session_entries_path, cat_lines(entries))
4.26 +
4.27 + def create_index(dir: Path): Unit =
4.28 + File.write(dir + index_path,
4.29 + File.read(dir + pre_index_path) +
4.30 + HTML.session_entries(get_entries(dir)) +
4.31 + HTML.end_document)
4.32 +
4.33 + def update_index(dir: Path, names: List[String]): Unit =
4.34 + try {
4.35 + put_entries(get_entries(dir).filterNot(names.contains) ::: names, dir)
4.36 + create_index(dir)
4.37 + }
4.38 + catch {
4.39 + case ERROR(msg) =>
4.40 + java.lang.System.err.println(
4.41 + "### " + msg + "\n### Browser info: failed to update session index of " + dir)
4.42 + }
4.43 +}
4.44 +
5.1 --- a/src/Pure/Tools/build.ML Thu Jan 03 17:40:36 2013 +0100
5.2 +++ b/src/Pure/Tools/build.ML Thu Jan 03 21:23:14 2013 +0100
5.3 @@ -89,6 +89,10 @@
5.4 | dups => error ("Duplicate document variants: " ^ commas_quote dups));
5.5
5.6 val _ =
5.7 + (case Session.path () of
5.8 + [] => ()
5.9 + | path => writeln ("\fSession.parent_path = " ^ space_implode "/" path));
5.10 + val _ =
5.11 Session.init do_output false
5.12 (Options.bool options "browser_info") browser_info
5.13 (Options.string options "document")
6.1 --- a/src/Pure/Tools/build.scala Thu Jan 03 17:40:36 2013 +0100
6.2 +++ b/src/Pure/Tools/build.scala Thu Jan 03 21:23:14 2013 +0100
6.3 @@ -412,7 +412,7 @@
6.4
6.5 /* jobs */
6.6
6.7 - private class Job(name: String, info: Session_Info, output: Path, do_output: Boolean,
6.8 + private class Job(name: String, val info: Session_Info, output: Path, do_output: Boolean,
6.9 verbose: Boolean, browser_info: Path)
6.10 {
6.11 // global browser info dir
6.12 @@ -515,6 +515,8 @@
6.13 private def log(name: String): Path = LOG + Path.basic(name)
6.14 private def log_gz(name: String): Path = log(name).ext("gz")
6.15
6.16 + private val SESSION_PARENT_PATH = "\fSession.parent_path = "
6.17 +
6.18 private def sources_stamp(digests: List[SHA1.Digest]): String =
6.19 digests.map(_.toString).sorted.mkString("sources: ", " ", "")
6.20
6.21 @@ -600,7 +602,7 @@
6.22 }
6.23
6.24 // scheduler loop
6.25 - case class Result(current: Boolean, heap: String, rc: Int)
6.26 + case class Result(current: Boolean, parent_path: Option[String], heap: String, rc: Int)
6.27
6.28 def sleep(): Unit = Thread.sleep(500)
6.29
6.30 @@ -620,9 +622,10 @@
6.31 //{{{ finish job
6.32
6.33 val (out, err, rc) = job.join
6.34 + val out_lines = split_lines(out)
6.35 progress.echo(Library.trim_line(err))
6.36
6.37 - val heap =
6.38 + val (parent_path, heap) =
6.39 if (rc == 0) {
6.40 (output_dir + log(name)).file.delete
6.41
6.42 @@ -631,7 +634,13 @@
6.43 File.write_gzip(output_dir + log_gz(name),
6.44 sources + "\n" + parent_heap + "\n" + heap + "\n" + out)
6.45
6.46 - heap
6.47 + val parent_path =
6.48 + if (job.info.options.bool("browser_info"))
6.49 + out_lines.find(_.startsWith(SESSION_PARENT_PATH)).map(line =>
6.50 + line.substring(SESSION_PARENT_PATH.length))
6.51 + else None
6.52 +
6.53 + (parent_path, heap)
6.54 }
6.55 else {
6.56 (output_dir + Path.basic(name)).file.delete
6.57 @@ -641,14 +650,14 @@
6.58 progress.echo(name + " FAILED")
6.59 if (rc != 130) {
6.60 progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
6.61 - val lines = split_lines(out)
6.62 - val tail = lines.drop(lines.length - 20 max 0)
6.63 + val tail = out_lines.drop(out_lines.length - 20 max 0)
6.64 progress.echo("\n" + cat_lines(tail))
6.65 }
6.66
6.67 - no_heap
6.68 + (None, no_heap)
6.69 }
6.70 - loop(pending - name, running - name, results + (name -> Result(false, heap, rc)))
6.71 + loop(pending - name, running - name,
6.72 + results + (name -> Result(false, parent_path, heap, rc)))
6.73 //}}}
6.74 case None if (running.size < (max_jobs max 1)) =>
6.75 //{{{ check/start next job
6.76 @@ -656,7 +665,7 @@
6.77 case Some((name, info)) =>
6.78 val parent_result =
6.79 info.parent match {
6.80 - case None => Result(true, no_heap, 0)
6.81 + case None => Result(true, None, no_heap, 0)
6.82 case Some(parent) => results(parent)
6.83 }
6.84 val output = output_dir + Path.basic(name)
6.85 @@ -679,10 +688,10 @@
6.86 val all_current = current && parent_result.current
6.87
6.88 if (all_current)
6.89 - loop(pending - name, running, results + (name -> Result(true, heap, 0)))
6.90 + loop(pending - name, running, results + (name -> Result(true, None, heap, 0)))
6.91 else if (no_build) {
6.92 if (verbose) progress.echo("Skipping " + name + " ...")
6.93 - loop(pending - name, running, results + (name -> Result(false, heap, 1)))
6.94 + loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
6.95 }
6.96 else if (parent_result.rc == 0) {
6.97 progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
6.98 @@ -691,7 +700,7 @@
6.99 }
6.100 else {
6.101 progress.echo(name + " CANCELLED")
6.102 - loop(pending - name, running, results + (name -> Result(false, heap, 1)))
6.103 + loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
6.104 }
6.105 case None => sleep(); loop(pending, running, results)
6.106 }
6.107 @@ -703,10 +712,17 @@
6.108 val results =
6.109 if (deps.is_empty) {
6.110 progress.echo("### Nothing to build")
6.111 - Map.empty
6.112 + Map.empty[String, Result]
6.113 }
6.114 else loop(queue, Map.empty, Map.empty)
6.115
6.116 + val session_entries =
6.117 + (for ((name, res) <- results.iterator if res.parent_path.isDefined)
6.118 + yield (res.parent_path.get, name)).toList.groupBy(_._1).map(
6.119 + { case (p, es) => (p, es.map(_._2).sorted) })
6.120 + for ((p, names) <- session_entries)
6.121 + Present.update_index(browser_info + Path.explode(p), names)
6.122 +
6.123 val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
6.124 if (rc != 0 && (verbose || !no_build)) {
6.125 val unfinished =
7.1 --- a/src/Pure/build-jars Thu Jan 03 17:40:36 2013 +0100
7.2 +++ b/src/Pure/build-jars Thu Jan 03 21:23:14 2013 +0100
7.3 @@ -57,6 +57,7 @@
7.4 System/utf8.scala
7.5 Thy/completion.scala
7.6 Thy/html.scala
7.7 + Thy/present.scala
7.8 Thy/thy_header.scala
7.9 Thy/thy_info.scala
7.10 Thy/thy_load.scala