--- a/src/Pure/System/session.ML Thu Jan 03 17:40:36 2013 +0100
+++ b/src/Pure/System/session.ML Thu Jan 03 21:23:14 2013 +0100
@@ -8,6 +8,7 @@
sig
val id: unit -> string list
val name: unit -> string
+ val path: unit -> string list
val welcome: unit -> string
val finish: unit -> unit
val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
--- a/src/Pure/Thy/html.scala Thu Jan 03 17:40:36 2013 +0100
+++ b/src/Pure/Thy/html.scala Thu Jan 03 21:23:14 2013 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Thy/html.scala
Author: Makarius
-Basic HTML output.
+HTML presentation elements.
*/
package isabelle
@@ -29,75 +29,19 @@
}
- /// FIXME unused stuff
-
- // common elements and attributes
-
- val BODY = "body"
- val DIV = "div"
- val SPAN = "span"
- val BR = "br"
- val PRE = "pre"
- val CLASS = "class"
- val STYLE = "style"
-
+ // common markup elements
- // document markup
-
- def span(cls: String, body: XML.Body): XML.Elem =
- XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
-
- def user_font(font: String, txt: String): XML.Elem =
- XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
-
- 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 bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt)))
+ def session_entry(name: String): String =
+ XML.string_of_tree(
+ XML.elem("li",
+ List(XML.Elem(Markup("a", List(("href", name + "/index.html"))),
+ List(XML.Text(name)))))) + "\n"
- def spans(input: XML.Tree): XML.Body =
- {
- def html_spans(tree: XML.Tree): XML.Body =
- tree match {
- case XML.Wrapped_Elem(markup, _, ts) =>
- List(span(markup.name, ts.flatMap(html_spans)))
- case XML.Elem(markup, ts) =>
- List(span(markup.name, ts.flatMap(html_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)
- t.clear
- }
- }
- def add(elem: XML.Tree) {
- flush()
- ts += elem
- }
- val syms = Symbol.iterator(txt)
- while (syms.hasNext) {
- val s1 = syms.next
- def s2() = if (syms.hasNext) syms.next else ""
- if (s1 == "\n") add(XML.elem(BR))
- else if (s1 == Symbol.sub_decoded || s1 == Symbol.isub_decoded)
- { add(hidden(s1)); add(sub(s2())) }
- else if (s1 == Symbol.sup_decoded || s1 == Symbol.isup_decoded)
- { add(hidden(s1)); add(sup(s2())) }
- else if (s1 == Symbol.bsub_decoded) t ++= s1 // FIXME
- else if (s1 == Symbol.esub_decoded) t ++= s1 // FIXME
- else if (s1 == Symbol.bsup_decoded) t ++= s1 // FIXME
- else if (s1 == Symbol.esup_decoded) t ++= s1 // FIXME
- else if (s1 == Symbol.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
- else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) }
- else t ++= s1
- }
- flush()
- ts.toList
- }
- html_spans(input)
- }
+ def session_entries(names: List[String]): String =
+ if (names.isEmpty) "</ul>"
+ else
+ "</ul>\n</div>\n<div class=\"sessions\">\n" +
+ "<h2>Sessions</h2>\n<ul>\n" + names.map(session_entry).mkString + "</ul>";
+
+ val end_document = "\n</div>\n</body>\n</html>\n"
}
--- a/src/Pure/Thy/present.ML Thu Jan 03 17:40:36 2013 +0100
+++ b/src/Pure/Thy/present.ML Thu Jan 03 21:23:14 2013 +0100
@@ -213,7 +213,7 @@
(** document preparation **)
-(* maintain index *)
+(* maintain session index *)
val session_entries =
HTML.session_entries o
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/present.scala Thu Jan 03 21:23:14 2013 +0100
@@ -0,0 +1,41 @@
+/* Title: Pure/Thy/present.scala
+ Author: Makarius
+
+Theory presentation: HTML.
+*/
+
+package isabelle
+
+
+object Present
+{
+ /* maintain session index -- NOT thread-safe */
+
+ private val index_path = Path.basic("index.html")
+ private val session_entries_path = Path.explode(".session/entries")
+ private val pre_index_path = Path.explode(".session/pre-index")
+
+ private def get_entries(dir: Path): List[String] =
+ split_lines(File.read(dir + session_entries_path))
+
+ private def put_entries(entries: List[String], dir: Path): Unit =
+ File.write(dir + session_entries_path, cat_lines(entries))
+
+ def create_index(dir: Path): Unit =
+ File.write(dir + index_path,
+ File.read(dir + pre_index_path) +
+ HTML.session_entries(get_entries(dir)) +
+ HTML.end_document)
+
+ def update_index(dir: Path, names: List[String]): Unit =
+ try {
+ put_entries(get_entries(dir).filterNot(names.contains) ::: names, dir)
+ create_index(dir)
+ }
+ catch {
+ case ERROR(msg) =>
+ java.lang.System.err.println(
+ "### " + msg + "\n### Browser info: failed to update session index of " + dir)
+ }
+}
+
--- a/src/Pure/Tools/build.ML Thu Jan 03 17:40:36 2013 +0100
+++ b/src/Pure/Tools/build.ML Thu Jan 03 21:23:14 2013 +0100
@@ -89,6 +89,10 @@
| dups => error ("Duplicate document variants: " ^ commas_quote dups));
val _ =
+ (case Session.path () of
+ [] => ()
+ | path => writeln ("\fSession.parent_path = " ^ space_implode "/" path));
+ val _ =
Session.init do_output false
(Options.bool options "browser_info") browser_info
(Options.string options "document")
--- a/src/Pure/Tools/build.scala Thu Jan 03 17:40:36 2013 +0100
+++ b/src/Pure/Tools/build.scala Thu Jan 03 21:23:14 2013 +0100
@@ -412,7 +412,7 @@
/* jobs */
- private class Job(name: String, info: Session_Info, output: Path, do_output: Boolean,
+ private class Job(name: String, val info: Session_Info, output: Path, do_output: Boolean,
verbose: Boolean, browser_info: Path)
{
// global browser info dir
@@ -515,6 +515,8 @@
private def log(name: String): Path = LOG + Path.basic(name)
private def log_gz(name: String): Path = log(name).ext("gz")
+ private val SESSION_PARENT_PATH = "\fSession.parent_path = "
+
private def sources_stamp(digests: List[SHA1.Digest]): String =
digests.map(_.toString).sorted.mkString("sources: ", " ", "")
@@ -600,7 +602,7 @@
}
// scheduler loop
- case class Result(current: Boolean, heap: String, rc: Int)
+ case class Result(current: Boolean, parent_path: Option[String], heap: String, rc: Int)
def sleep(): Unit = Thread.sleep(500)
@@ -620,9 +622,10 @@
//{{{ finish job
val (out, err, rc) = job.join
+ val out_lines = split_lines(out)
progress.echo(Library.trim_line(err))
- val heap =
+ val (parent_path, heap) =
if (rc == 0) {
(output_dir + log(name)).file.delete
@@ -631,7 +634,13 @@
File.write_gzip(output_dir + log_gz(name),
sources + "\n" + parent_heap + "\n" + heap + "\n" + out)
- heap
+ val parent_path =
+ if (job.info.options.bool("browser_info"))
+ out_lines.find(_.startsWith(SESSION_PARENT_PATH)).map(line =>
+ line.substring(SESSION_PARENT_PATH.length))
+ else None
+
+ (parent_path, heap)
}
else {
(output_dir + Path.basic(name)).file.delete
@@ -641,14 +650,14 @@
progress.echo(name + " FAILED")
if (rc != 130) {
progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
- val lines = split_lines(out)
- val tail = lines.drop(lines.length - 20 max 0)
+ val tail = out_lines.drop(out_lines.length - 20 max 0)
progress.echo("\n" + cat_lines(tail))
}
- no_heap
+ (None, no_heap)
}
- loop(pending - name, running - name, results + (name -> Result(false, heap, rc)))
+ loop(pending - name, running - name,
+ results + (name -> Result(false, parent_path, heap, rc)))
//}}}
case None if (running.size < (max_jobs max 1)) =>
//{{{ check/start next job
@@ -656,7 +665,7 @@
case Some((name, info)) =>
val parent_result =
info.parent match {
- case None => Result(true, no_heap, 0)
+ case None => Result(true, None, no_heap, 0)
case Some(parent) => results(parent)
}
val output = output_dir + Path.basic(name)
@@ -679,10 +688,10 @@
val all_current = current && parent_result.current
if (all_current)
- loop(pending - name, running, results + (name -> Result(true, heap, 0)))
+ loop(pending - name, running, results + (name -> Result(true, None, heap, 0)))
else if (no_build) {
if (verbose) progress.echo("Skipping " + name + " ...")
- loop(pending - name, running, results + (name -> Result(false, heap, 1)))
+ loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
}
else if (parent_result.rc == 0) {
progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
@@ -691,7 +700,7 @@
}
else {
progress.echo(name + " CANCELLED")
- loop(pending - name, running, results + (name -> Result(false, heap, 1)))
+ loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
}
case None => sleep(); loop(pending, running, results)
}
@@ -703,10 +712,17 @@
val results =
if (deps.is_empty) {
progress.echo("### Nothing to build")
- Map.empty
+ Map.empty[String, Result]
}
else loop(queue, Map.empty, Map.empty)
+ val session_entries =
+ (for ((name, res) <- results.iterator if res.parent_path.isDefined)
+ yield (res.parent_path.get, name)).toList.groupBy(_._1).map(
+ { case (p, es) => (p, es.map(_._2).sorted) })
+ for ((p, names) <- session_entries)
+ Present.update_index(browser_info + Path.explode(p), names)
+
val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
if (rc != 0 && (verbose || !no_build)) {
val unfinished =
--- a/src/Pure/build-jars Thu Jan 03 17:40:36 2013 +0100
+++ b/src/Pure/build-jars Thu Jan 03 21:23:14 2013 +0100
@@ -57,6 +57,7 @@
System/utf8.scala
Thy/completion.scala
Thy/html.scala
+ Thy/present.scala
Thy/thy_header.scala
Thy/thy_info.scala
Thy/thy_load.scala