# HG changeset patch # User wenzelm # Date 1357244594 -3600 # Node ID 07202e00fe4d51caf38ee91b9102e2ce67682a7a # Parent 573d84e08f3f9756ea68562dd16fcfb866d0692c# Parent 5b2bf7611662ef34e894c2a7f69913821c56d7b9 merged diff -r 573d84e08f3f -r 07202e00fe4d src/Pure/System/session.ML --- 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 -> diff -r 573d84e08f3f -r 07202e00fe4d src/Pure/Thy/html.scala --- 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) "" + else + "\n\n
\n" + + "

Sessions

\n"; + + val end_document = "\n
\n\n\n" } diff -r 573d84e08f3f -r 07202e00fe4d src/Pure/Thy/present.ML --- 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 diff -r 573d84e08f3f -r 07202e00fe4d src/Pure/Thy/present.scala --- /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) + } +} + diff -r 573d84e08f3f -r 07202e00fe4d src/Pure/Tools/build.ML --- 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") diff -r 573d84e08f3f -r 07202e00fe4d src/Pure/Tools/build.scala --- 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 = diff -r 573d84e08f3f -r 07202e00fe4d src/Pure/build-jars --- 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