| author | wenzelm |
| Fri, 27 Jul 2012 16:35:02 +0200 | |
| changeset 48557 | 2aa8bab841d7 |
| parent 48556 | 62a3fbf9d35b (current diff) |
| parent 48554 | 011cbb395d46 (diff) |
| child 48558 | fabbed3abc1e |
--- a/doc-src/antiquote_setup.ML Fri Jul 27 15:42:39 2012 +0200 +++ b/doc-src/antiquote_setup.ML Fri Jul 27 16:35:02 2012 +0200 @@ -204,7 +204,7 @@ "" "antiquotation" #> entity_antiqs (thy_check Thy_Output.intern_option Thy_Output.defined_option) "" "antiquotation option" #> - entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting" #> + entity_antiqs no_check "isatt" "setting" #> entity_antiqs no_check "" "inference" #> entity_antiqs no_check "isatt" "executable" #> entity_antiqs (K check_tool) "isatt" "tool" #>
--- a/etc/settings Fri Jul 27 15:42:39 2012 +0200 +++ b/etc/settings Fri Jul 27 16:35:02 2012 +0200 @@ -97,7 +97,7 @@ ### # The place for user configuration, heap files, etc. -if [ -z "ISABELLE_IDENTIFIER" ]; then +if [ -z "$ISABELLE_IDENTIFIER" ]; then ISABELLE_HOME_USER="$USER_HOME/.isabelle" else ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER"
--- a/lib/Tools/build Fri Jul 27 15:42:39 2012 +0200 +++ b/lib/Tools/build Fri Jul 27 16:35:02 2012 +0200 @@ -26,7 +26,7 @@ echo "Usage: isabelle $PRG [OPTIONS] [SESSIONS ...]" echo echo " Options are:" - echo " -a all sessions" + echo " -a include all sessions" echo " -b build heap images" echo " -d DIR include session directory with ROOT file" echo " -g NAME include session group NAME" @@ -34,7 +34,6 @@ echo " -n no build -- test dependencies only" echo " -o OPTION override session configuration OPTION (via NAME=VAL or NAME)" echo " -s system build mode: produce output in ISABELLE_HOME" - echo " -t inner session timing" echo " -v verbose" echo echo " Build and manage Isabelle sessions, depending on implicit" @@ -65,10 +64,9 @@ NO_BUILD=false eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)" SYSTEM_MODE=false -TIMING=false VERBOSE=false -while getopts "abd:g:j:no:stv" OPT +while getopts "abd:g:j:no:sv" OPT do case "$OPT" in a) @@ -96,9 +94,6 @@ s) SYSTEM_MODE="true" ;; - t) - TIMING="true" - ;; v) VERBOSE="true" ;; @@ -126,7 +121,7 @@ fi "$ISABELLE_TOOL" java isabelle.Build \ - "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$TIMING" "$VERBOSE" \ + "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \ "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" RC="$?"
--- a/lib/scripts/getsettings Fri Jul 27 15:42:39 2012 +0200 +++ b/lib/scripts/getsettings Fri Jul 27 16:35:02 2012 +0200 @@ -197,6 +197,7 @@ #main components init_component "$ISABELLE_HOME" +[ -d "$ISABELLE_HOME/doc-src" ] && init_component "$ISABELLE_HOME/doc-src" [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER" #ML system identifier
--- a/src/Pure/General/file.scala Fri Jul 27 15:42:39 2012 +0200 +++ b/src/Pure/General/file.scala Fri Jul 27 16:35:02 2012 +0200 @@ -35,6 +35,19 @@ def read(path: Path): String = read(path.file) + /* try_read */ + + def try_read(paths: Seq[Path]): String = + { + val buf = new StringBuilder + for (path <- paths if path.is_file) { + buf.append(read(path)) + buf.append('\n') + } + buf.toString + } + + /* write */ private def write_file(file: JFile, text: CharSequence, gzip: Boolean)
--- a/src/Pure/General/path.scala Fri Jul 27 15:42:39 2012 +0200 +++ b/src/Pure/General/path.scala Fri Jul 27 16:35:02 2012 +0200 @@ -175,7 +175,14 @@ } + /* source position */ + + def position: Position.T = Position.File(implode) + + /* platform file */ def file: JFile = Isabelle_System.platform_file(this) + def is_file: Boolean = file.isFile + def is_dir: Boolean = file.isDirectory }
--- a/src/Pure/General/position.scala Fri Jul 27 15:42:39 2012 +0200 +++ b/src/Pure/General/position.scala Fri Jul 27 16:35:02 2012 +0200 @@ -20,9 +20,6 @@ val File = new Properties.String(Isabelle_Markup.FILE) val Id = new Properties.Long(Isabelle_Markup.ID) - def file(f: JFile): T = File(Isabelle_System.posix_path(f.toString)) - def line_file(i: Int, f: JFile): T = Line(i) ::: file(f) - object Range { def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
--- a/src/Pure/General/symbol.scala Fri Jul 27 15:42:39 2012 +0200 +++ b/src/Pure/General/symbol.scala Fri Jul 27 16:35:02 2012 +0200 @@ -210,8 +210,7 @@ /** symbol interpretation **/ private lazy val symbols = - new Interpretation( - Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("ISABELLE_SYMBOLS")))) + new Interpretation(File.try_read(Path.split(Isabelle_System.getenv_strict("ISABELLE_SYMBOLS")))) private class Interpretation(symbols_spec: String) {
--- a/src/Pure/System/build.ML Fri Jul 27 15:42:39 2012 +0200 +++ b/src/Pure/System/build.ML Fri Jul 27 16:35:02 2012 +0200 @@ -56,12 +56,12 @@ fun build args_file = let - val (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name, - (name, (base_name, theories)))))))) = + val (do_output, (options, (verbose, (browser_info, (parent_name, + (name, theories)))))) = File.read (Path.explode args_file) |> YXML.parse_body |> let open XML.Decode in - pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string - (pair string (pair string ((list (pair Options.decode (list string))))))))))) + pair bool (pair Options.decode (pair bool (pair string (pair string + (pair string ((list (pair Options.decode (list string))))))))) end; val _ = @@ -70,10 +70,11 @@ (Options.string options "document") (Options.bool options "document_graph") (space_explode ":" (Options.string options "document_variants")) - parent_base_name base_name - (Options.string options "document_dump", Options.string options "document_dump_mode") + parent_name name + (Options.string options "document_dump", + Present.dump_mode (Options.string options "document_dump_mode")) "" verbose; - val _ = Session.with_timing name timing (List.app use_theories) theories; + val _ = Session.with_timing name verbose (List.app use_theories) theories; val _ = Session.finish (); val _ = if do_output then () else quit (); in () end
--- a/src/Pure/System/build.scala Fri Jul 27 15:42:39 2012 +0200 +++ b/src/Pure/System/build.scala Fri Jul 27 16:35:02 2012 +0200 @@ -7,7 +7,7 @@ package isabelle -import java.io.{File => JFile, BufferedInputStream, FileInputStream, +import java.io.{BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader, IOException} import java.util.zip.GZIPInputStream @@ -24,16 +24,14 @@ /* Info */ sealed case class Info( - base_name: String, groups: List[String], dir: Path, parent: Option[String], - parent_base_name: Option[String], description: String, options: Options, theories: List[(Options, List[Path])], files: List[Path], - digest: SHA1.Digest) + entry_digest: SHA1.Digest) /* Queue */ @@ -93,7 +91,7 @@ /* parsing */ private case class Session_Entry( - name: String, + base_name: String, this_name: Boolean, groups: List[String], path: Option[String], @@ -140,10 +138,10 @@ { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) } } - def parse_entries(root: JFile): List[Session_Entry] = + def parse_entries(root: Path): List[Session_Entry] = { val toks = syntax.scan(File.read(root)) - parse_all(rep(session_entry), Token.reader(toks, root.toString)) match { + parse_all(rep(session_entry), Token.reader(toks, root.implode)) match { case Success(result, _) => result case bad => error(bad.toString) } @@ -158,33 +156,32 @@ private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure" - private def sessions_root(options: Options, dir: Path, root: JFile, queue: Session.Queue) + private def sessions_root(options: Options, dir: Path, root: Path, queue: Session.Queue) : Session.Queue = { (queue /: Parser.parse_entries(root))((queue1, entry) => try { - if (entry.name == "") error("Bad session name") + if (entry.base_name == "") error("Bad session name") - val (full_name, parent_base_name) = - if (is_pure(entry.name)) { + val full_name = + if (is_pure(entry.base_name)) { if (entry.parent.isDefined) error("Illegal parent session") - else (entry.name, None: Option[String]) + else entry.base_name } else entry.parent match { case Some(parent_name) if queue1.isDefinedAt(parent_name) => val full_name = - if (entry.this_name) entry.name - else parent_name + "-" + entry.name - val parent_base_name = Some(queue1(parent_name).base_name) - (full_name, parent_base_name) + if (entry.this_name) entry.base_name + else parent_name + "-" + entry.base_name + full_name case _ => error("Bad parent session") } val path = entry.path match { case Some(p) => Path.explode(p) - case None => Path.basic(entry.name) + case None => Path.basic(entry.base_name) } val session_options = options ++ entry.options @@ -193,31 +190,32 @@ entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(Path.explode(_))) }) val files = entry.files.map(Path.explode(_)) - val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString) + val entry_digest = + SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString) val info = - Session.Info(entry.name, entry.groups, dir + path, entry.parent, parent_base_name, - entry.description, session_options, theories, files, digest) + Session.Info(entry.groups, dir + path, entry.parent, entry.description, + session_options, theories, files, entry_digest) queue1 + (full_name, info) } catch { case ERROR(msg) => error(msg + "\nThe error(s) above occurred in session entry " + - quote(entry.name) + Position.str_of(Position.file(root))) + quote(entry.base_name) + Position.str_of(root.position)) }) } private def sessions_dir(options: Options, strict: Boolean, dir: Path, queue: Session.Queue) : Session.Queue = { - val root = (dir + ROOT).file - if (root.isFile) sessions_root(options, dir, root, queue) - else if (strict) error("Bad session root file: " + quote(root.toString)) + val root = dir + ROOT + if (root.is_file) sessions_root(options, dir, root, queue) + else if (strict) error("Bad session root file: " + root.toString) else queue } - private def sessions_catalog(options: Options, dir: Path, catalog: JFile, queue: Session.Queue) + private def sessions_catalog(options: Options, dir: Path, catalog: Path, queue: Session.Queue) : Session.Queue = { val dirs = @@ -225,12 +223,12 @@ (queue /: dirs)((queue1, dir1) => try { val dir2 = dir + Path.explode(dir1) - if (dir2.file.isDirectory) sessions_dir(options, true, dir2, queue1) + if (dir2.is_dir) sessions_dir(options, true, dir2, queue1) else error("Bad session directory: " + dir2.toString) } catch { case ERROR(msg) => - error(msg + "\nThe error(s) above occurred in session catalog " + quote(catalog.toString)) + error(msg + "\nThe error(s) above occurred in session catalog " + catalog.toString) }) } @@ -242,9 +240,8 @@ for (dir <- Isabelle_System.components()) { queue = sessions_dir(options, false, dir, queue) - val catalog = (dir + SESSIONS).file - if (catalog.isFile) - queue = sessions_catalog(options, dir, catalog, queue) + val catalog = dir + SESSIONS + if (catalog.is_file) queue = sessions_catalog(options, dir, catalog, queue) } for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue) @@ -286,7 +283,7 @@ } val thy_info = new Thy_Info(new Thy_Load(preloaded)) - if (verbose) echo("Checking " + name) + if (verbose) echo("Checking " + name + " ...") val thy_deps = thy_info.dependencies( @@ -319,7 +316,7 @@ /* jobs */ - private class Job(cwd: JFile, env: Map[String, String], script: String, args: String, + private class Job(dir: Path, env: Map[String, String], script: String, args: String, output: Path, do_output: Boolean) { private val args_file = File.tmp_file("args") @@ -327,7 +324,7 @@ File.write(args_file, args) private val (thread, result) = - Simple_Thread.future("build") { Isabelle_System.bash_env(cwd, env1, script) } + Simple_Thread.future("build") { Isabelle_System.bash_env(dir.file, env1, script) } def terminate: Unit = thread.interrupt def is_finished: Boolean = result.is_finished @@ -336,10 +333,10 @@ } private def start_job(name: String, info: Session.Info, output: Path, do_output: Boolean, - options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job = + options: Options, verbose: Boolean, browser_info: Path): Job = { // global browser info dir - if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile) + if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file) { browser_info.file.mkdirs() File.copy(Path.explode("~~/lib/logo/isabelle.gif"), @@ -351,9 +348,7 @@ } val parent = info.parent.getOrElse("") - val parent_base_name = info.parent_base_name.getOrElse("") - val cwd = info.dir.file val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output)) val script = @@ -388,12 +383,12 @@ val args_xml = { import XML.Encode._ - pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string, - pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))( - (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name, - (name, (info.base_name, info.theories))))))))) + pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string, + pair(string, list(pair(Options.encode, list(Path.encode)))))))))( + (do_output, (options, (verbose, (browser_info, (parent, + (name, info.theories))))))) } - new Job(cwd, env, script, YXML.string_of_body(args_xml), output, do_output) + new Job(info.dir, env, script, YXML.string_of_body(args_xml), output, do_output) } @@ -444,7 +439,6 @@ no_build: Boolean = false, build_options: List[String] = Nil, system_mode: Boolean = false, - timing: Boolean = false, verbose: Boolean = false, sessions: List[String] = Nil): Int = { @@ -453,7 +447,7 @@ val deps = dependencies(verbose, queue) def make_stamp(name: String): String = - sources_stamp(queue(name).digest :: deps.sources(name)) + sources_stamp(queue(name).entry_digest :: deps.sources(name)) val (input_dirs, output_dir, browser_info) = if (system_mode) { @@ -476,76 +470,80 @@ results: Map[String, (Boolean, Int)]): Map[String, (Boolean, Int)] = { if (pending.is_empty) results - else if (running.exists({ case (_, job) => job.is_finished })) - { // finish job - val (name, job) = running.find({ case (_, job) => job.is_finished }).get + else + running.find({ case (_, job) => job.is_finished }) match { + case Some((name, job)) => + // finish job - val (out, err, rc) = job.join - echo(Library.trim_line(err)) + val (out, err, rc) = job.join + echo(Library.trim_line(err)) - if (rc == 0) { - val sources = make_stamp(name) - val heap = heap_stamp(job.output_path) - File.write_gzip(output_dir + log_gz(name), sources + "\n" + heap + "\n" + out) - } - else { - File.write(output_dir + log(name), out) - echo(name + " FAILED") - echo("(see also " + log(name).file.toString + ")") - val lines = split_lines(out) - val tail = lines.drop(lines.length - 20 max 0) - echo("\n" + cat_lines(tail)) - } - loop(pending - name, running - name, results + (name -> (false, rc))) - } - else if (running.size < (max_jobs max 1)) - { // check/start next job - pending.dequeue(running.isDefinedAt(_)) match { - case Some((name, info)) => - val parent_result = info.parent.map(results(_)) - val parent_current = parent_result.forall(_._1) - val parent_ok = parent_result.forall(_._2 == 0) + if (rc == 0) { + val sources = make_stamp(name) + val heap = heap_stamp(job.output_path) + (output_dir + log(name)).file.delete + File.write_gzip(output_dir + log_gz(name), sources + "\n" + heap + "\n" + out) + } + else { + (output_dir + log_gz(name)).file.delete + File.write(output_dir + log(name), out) + echo(name + " FAILED") + echo("(see also " + log(name).file.toString + ")") + val lines = split_lines(out) + val tail = lines.drop(lines.length - 20 max 0) + echo("\n" + cat_lines(tail)) + } + loop(pending - name, running - name, results + (name -> (false, rc))) - val output = output_dir + Path.basic(name) - val do_output = build_heap || queue.is_inner(name) + case None if (running.size < (max_jobs max 1)) => + // check/start next job + pending.dequeue(running.isDefinedAt(_)) match { + case Some((name, info)) => + val parent_result = info.parent.map(results(_)) + val parent_current = parent_result.forall(_._1) + val parent_ok = parent_result.forall(_._2 == 0) - val current = - { - input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match { - case Some(dir) => - check_stamps(dir, name) match { - case Some((s, h)) => s == make_stamp(name) && (h || !do_output) + val output = output_dir + Path.basic(name) + val do_output = build_heap || queue.is_inner(name) + + val current = + { + input_dirs.find(dir => (dir + log_gz(name)).is_file) match { + case Some(dir) => + check_stamps(dir, name) match { + case Some((s, h)) => s == make_stamp(name) && (h || !do_output) + case None => false + } case None => false } - case None => false - } - } - val all_current = current && parent_current + } + val all_current = current && parent_current - if (all_current) - loop(pending - name, running, results + (name -> (true, 0))) - else if (no_build) - loop(pending - name, running, results + (name -> (false, 1))) - else if (parent_ok) { - echo((if (do_output) "Building " else "Running ") + name + " ...") - val job = - start_job(name, info, output, do_output, info.options, timing, verbose, browser_info) - loop(pending, running + (name -> job), results) - } - else { - echo(name + " CANCELLED") - loop(pending - name, running, results + (name -> (false, 1))) + if (all_current) + loop(pending - name, running, results + (name -> (true, 0))) + else if (no_build) + loop(pending - name, running, results + (name -> (false, 1))) + else if (parent_ok) { + echo((if (do_output) "Building " else "Running ") + name + " ...") + val job = + start_job(name, info, output, do_output, info.options, verbose, browser_info) + loop(pending, running + (name -> job), results) + } + else { + echo(name + " CANCELLED") + loop(pending - name, running, results + (name -> (false, 1))) + } + case None => sleep(); loop(pending, running, results) } case None => sleep(); loop(pending, running, results) } - } - else { sleep(); loop(pending, running, results) } } val results = loop(queue, Map.empty, Map.empty) val rc = (0 /: results)({ case (rc1, (_, (_, rc2))) => rc1 max rc2 }) if (rc != 0 && (verbose || !no_build)) { - val unfinished = (for ((name, r) <- results.iterator if r != 0) yield name).toList.sorted + val unfinished = + (for ((name, (_, r)) <- results.iterator if r != 0) yield name).toList.sorted echo("Unfinished session(s): " + commas(unfinished)) } rc @@ -564,11 +562,10 @@ Properties.Value.Int(max_jobs) :: Properties.Value.Boolean(no_build) :: Properties.Value.Boolean(system_mode) :: - Properties.Value.Boolean(timing) :: Properties.Value.Boolean(verbose) :: Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) => build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups, - max_jobs, no_build, build_options, system_mode, timing, verbose, sessions) + max_jobs, no_build, build_options, system_mode, verbose, sessions) case _ => error("Bad arguments:\n" + cat_lines(args)) } }
--- a/src/Pure/System/isabelle_system.scala Fri Jul 27 15:42:39 2012 +0200 +++ b/src/Pure/System/isabelle_system.scala Fri Jul 27 16:35:02 2012 +0200 @@ -124,19 +124,6 @@ def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path) - /* try_read */ - - def try_read(paths: Seq[Path]): String = - { - val buf = new StringBuilder - for { - path <- paths - file = platform_file(path) if file.isFile - } { buf.append(File.read(file)); buf.append('\n') } - buf.toString - } - - /* source files */ private def try_file(file: JFile) = if (file.isFile) Some(file) else None
--- a/src/Pure/System/options.scala Fri Jul 27 15:42:39 2012 +0200 +++ b/src/Pure/System/options.scala Fri Jul 27 16:35:02 2012 +0200 @@ -7,9 +7,6 @@ package isabelle -import java.io.{File => JFile} - - object Options { type Spec = (String, Option[String]) @@ -54,9 +51,9 @@ { case _ ~ (a ~ _ ~ b) => (options: Options) => options.define(a, b) } } - def parse_entries(file: JFile): List[Options => Options] = + def parse_entries(file: Path): List[Options => Options] = { - parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.toString)) match { + parse_all(rep(entry), Token.reader(syntax.scan(File.read(file)), file.implode)) match { case Success(result, _) => result case bad => error(bad.toString) } @@ -70,12 +67,11 @@ var options = empty for { dir <- Isabelle_System.components() - file = (dir + OPTIONS).file - if file.isFile + file = dir + OPTIONS if file.is_file entry <- Parser.parse_entries(file) } { try { options = entry(options) } - catch { case ERROR(msg) => error(msg + Position.str_of(Position.file(file))) } + catch { case ERROR(msg) => error(msg + Position.str_of(file.position)) } } options }
--- a/src/Pure/System/session.ML Fri Jul 27 15:42:39 2012 +0200 +++ b/src/Pure/System/session.ML Fri Jul 27 16:35:02 2012 +0200 @@ -11,7 +11,7 @@ val welcome: unit -> string val finish: unit -> unit val init: bool -> bool -> bool -> string -> string -> bool -> string list -> - string -> string -> string * string -> string -> bool -> unit + string -> string -> string * Present.dump_mode -> string -> bool -> unit val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b val use_dir: string -> string -> bool -> string list -> bool -> bool -> string -> string -> bool -> string list -> string -> string -> bool * string -> @@ -21,24 +21,21 @@ structure Session: SESSION = struct - (* session state *) val session = Unsynchronized.ref ([Context.PureN]: string list); -val session_path = Unsynchronized.ref ([]: string list); val session_finished = Unsynchronized.ref false; -val remote_path = Unsynchronized.ref (NONE: Url.T option); + +fun id () = ! session; +fun name () = "Isabelle/" ^ List.last (! session); (* access path *) -fun id () = ! session; -fun path () = ! session_path; +val session_path = Unsynchronized.ref ([]: string list); +val remote_path = Unsynchronized.ref (NONE: Url.T option); -fun str_of [] = Context.PureN - | str_of elems = space_implode "/" elems; - -fun name () = "Isabelle/" ^ str_of (path ()); +fun path () = ! session_path; (* welcome *) @@ -61,7 +58,7 @@ let val sess = ! session @ [s] in (case duplicates (op =) sess of [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s])) - | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess)) + | dups => error ("Duplicate session identifiers " ^ commas_quote dups)) end; @@ -115,7 +112,7 @@ local -fun doc_dump (cp, dump) = (dump, if cp then "all" else "tex+sty"); +fun doc_dump (cp, dump) = (dump, if cp then Present.Dump_all else Present.Dump_tex_sty); in
--- a/src/Pure/Thy/present.ML Fri Jul 27 15:42:39 2012 +0200 +++ b/src/Pure/Thy/present.ML Fri Jul 27 16:35:02 2012 +0200 @@ -17,8 +17,10 @@ path: string, parents: string list} list -> Path.T -> unit val display_graph: {name: string, ID: string, dir: string, unfold: bool, path: string, parents: string list} list -> unit + datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty + val dump_mode: string -> dump_mode val init: bool -> bool -> string -> string -> bool -> string list -> string list -> - string -> string * string -> Url.T option * bool -> bool -> + string -> string * dump_mode -> Url.T option * bool -> bool -> theory list -> unit (*not thread-safe!*) val finish: unit -> unit (*not thread-safe!*) val init_theory: string -> unit @@ -207,10 +209,18 @@ (* session_info *) +datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty; + +fun dump_mode "all" = Dump_all + | dump_mode "tex" = Dump_tex + | dump_mode "tex+sty" = Dump_tex_sty + | dump_mode s = + error ("Illegal document dump mode: " ^ quote s ^ " (expected \"all\", \"tex\", \"tex+sty\")"); + type session_info = {name: string, parent: string, session: string, path: string list, html_prefix: Path.T, info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list, - doc_dump: (string * string), remote_path: Url.T option, verbose: bool, + doc_dump: (string * dump_mode), remote_path: Url.T option, verbose: bool, readme: Path.T option}; fun make_session_info @@ -377,12 +387,12 @@ fun prepare_sources doc_dir doc_mode = (Isabelle_System.mkdirs doc_dir; - if doc_mode = "all" then Isabelle_System.copy_dir document_path doc_dir - else if doc_mode = "tex+sty" then - ignore (Isabelle_System.isabelle_tool "latex" - ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")))) - else if doc_mode = "tex" then () - else error ("Illegal document dump mode: " ^ quote doc_mode); + (case doc_mode of + Dump_all => Isabelle_System.copy_dir document_path doc_dir + | Dump_tex_sty => + ignore (Isabelle_System.isabelle_tool "latex" + ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")))) + | Dump_tex => ()); (case opt_graphs of NONE => () | SOME (pdf, eps) => (File.write (Path.append doc_dir graph_pdf_path) pdf; File.write (Path.append doc_dir graph_eps_path) eps)); @@ -424,7 +434,7 @@ documents |> Par_List.map (fn (name, tags) => let val path = Path.append html_prefix (Path.basic name); - val _ = prepare_sources path "all"; + val _ = prepare_sources path Dump_all; in isabelle_document true doc_format name tags path html_prefix end); val _ = if verbose then
--- a/src/Tools/jEdit/src/html_panel.scala Fri Jul 27 15:42:39 2012 +0200 +++ b/src/Tools/jEdit/src/html_panel.scala Fri Jul 27 16:35:02 2012 +0200 @@ -92,7 +92,7 @@ <head> <style media="all" type="text/css"> """ + - Isabelle_System.try_read(Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS"))) + File.try_read(Path.split(Isabelle_System.getenv_strict("JEDIT_STYLE_SHEETS"))) private val template_tail = """
--- a/src/Tools/jEdit/src/readme_dockable.scala Fri Jul 27 15:42:39 2012 +0200 +++ b/src/Tools/jEdit/src/readme_dockable.scala Fri Jul 27 16:35:02 2012 +0200 @@ -17,8 +17,7 @@ private val readme = new HTML_Panel("SansSerif", 14) private val readme_path = Path.explode("$JEDIT_HOME/README.html") readme.render_document( - Isabelle_System.platform_file_url(readme_path), - Isabelle_System.try_read(List(readme_path))) + Isabelle_System.platform_file_url(readme_path), File.try_read(List(readme_path))) set_content(readme) }