# HG changeset patch # User wenzelm # Date 1527625772 -7200 # Node ID 88c07fabd5b411422dba001138ac334c426a1fdd # Parent 56c57e91edf915fd7d4c5929521b79348ee5a840# Parent bf733673198191d80f1018272557b3ab93121075 merged diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Doc/System/Server.thy --- a/src/Doc/System/Server.thy Tue May 29 20:01:50 2018 +0200 +++ b/src/Doc/System/Server.thy Tue May 29 22:29:32 2018 +0200 @@ -516,13 +516,14 @@ session-qualified theory name (e.g.\ \<^verbatim>\HOL-ex.Seq\). \<^item> \<^bold>\type\ \node_status = {ok: bool, total: int, unprocessed: int, running: - int, warned: int, failed: int, finished: int, consolidated: bool}\ - represents a formal theory node status of the PIDE document model. Fields - \total\, \unprocessed\, \running\, \warned\, \failed\, \finished\ account - for individual commands within a theory node; \ok\ is an abstraction for - \failed = 0\. The \consolidated\ flag indicates whether the outermost theory - command structure has finished (or failed) and the final \<^theory_text>\end\ command has - been checked. + int, warned: int, failed: int, finished: int, initialized: bool, + consolidated: bool}\ represents a formal theory node status of the PIDE + document model. Fields \total\, \unprocessed\, \running\, \warned\, + \failed\, \finished\ account for individual commands within a theory node; + \ok\ is an abstraction for \failed = 0\. The \initialized\ flag indicates + that the initial \<^theory_text>\theory\ command has been processed. The \consolidated\ + flag indicates whether the outermost theory command structure has finished + (or failed) and the final \<^theory_text>\end\ command has been checked. \ diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Doc/System/Sessions.thy --- a/src/Doc/System/Sessions.thy Tue May 29 20:01:50 2018 +0200 +++ b/src/Doc/System/Sessions.thy Tue May 29 22:29:32 2018 +0200 @@ -557,7 +557,7 @@ \Usage: isabelle export [OPTIONS] SESSION Options are: - -D DIR target directory for exported files (default: "export") + -O DIR output directory for exported files (default: "export") -d DIR include session directory -l list exports -n no build of session @@ -590,7 +590,7 @@ \<^emph>\all\ theory exports. Multiple options \<^verbatim>\-x\ refer to the union of all specified patterns. - Option \<^verbatim>\-D\ specifies an alternative base directory for option \<^verbatim>\-x\: the + Option \<^verbatim>\-O\ specifies an alternative output directory for option \<^verbatim>\-x\: the default is \<^verbatim>\export\ within the current directory. Each theory creates its own sub-directory hierarchy, using the session-qualified theory name. \ diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Pure/General/exn.scala --- a/src/Pure/General/exn.scala Tue May 29 20:01:50 2018 +0200 +++ b/src/Pure/General/exn.scala Tue May 29 22:29:32 2018 +0200 @@ -81,6 +81,10 @@ found_interrupt } + def interruptible_capture[A](e: => A): Result[A] = + try { Res(e) } + catch { case exn: Throwable if !is_interrupt(exn) => Exn[A](exn) } + object Interrupt { def apply(): Throwable = new InterruptedException diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Pure/General/graph.scala --- a/src/Pure/General/graph.scala Tue May 29 20:01:50 2018 +0200 +++ b/src/Pure/General/graph.scala Tue May 29 22:29:32 2018 +0200 @@ -66,6 +66,7 @@ def is_empty: Boolean = rep.isEmpty def defined(x: Key): Boolean = rep.isDefinedAt(x) + def domain: Set[Key] = rep.keySet def iterator: Iterator[(Key, Entry)] = rep.iterator diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue May 29 20:01:50 2018 +0200 +++ b/src/Pure/PIDE/command.scala Tue May 29 22:29:32 2018 +0200 @@ -260,6 +260,8 @@ exports: Exports = Exports.empty, markups: Markups = Markups.empty) { + def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED) + lazy val consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED) @@ -565,6 +567,8 @@ val is_unparsed: Boolean = span.content.exists(_.is_unparsed) val is_unfinished: Boolean = span.content.exists(_.is_unfinished) + def potentially_initialized: Boolean = span.name == Thy_Header.THEORY + /* blobs */ diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Tue May 29 20:01:50 2018 +0200 +++ b/src/Pure/PIDE/document.ML Tue May 29 22:29:32 2018 +0200 @@ -633,7 +633,9 @@ val parents = if null parents_reports then [Theory.get_pure ()] else map #1 parents_reports; val _ = Position.reports (map #2 parents_reports); - in Resources.begin_theory master_dir header parents end; + val thy = Resources.begin_theory master_dir header parents; + val _ = Output.status (Markup.markup_only Markup.initialized); + in thy end; fun check_root_theory node = let diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue May 29 20:01:50 2018 +0200 +++ b/src/Pure/PIDE/document.scala Tue May 29 22:29:32 2018 +0200 @@ -383,6 +383,8 @@ new Nodes(graph3.map_node(name, _ => node)) } + def domain: Set[Node.Name] = graph.domain + def iterator: Iterator[(Node.Name, Node)] = graph.iterator.map({ case (name, (node, _)) => (name, node) }) @@ -529,7 +531,6 @@ def node_name: Node.Name def node: Node - def node_consolidated: Boolean def commands_loading: List[Command] def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] @@ -920,6 +921,13 @@ } } + def node_initialized(version: Version, name: Node.Name): Boolean = + name.is_theory && + (version.nodes(name).commands.iterator.find(_.potentially_initialized) match { + case None => false + case Some(command) => command_states(version, command).headOption.exists(_.initialized) + }) + def node_consolidated(version: Version, name: Node.Name): Boolean = !name.is_theory || version.nodes(name).commands.reverse.iterator. @@ -969,8 +977,6 @@ val node_name: Node.Name = name val node: Node = version.nodes(name) - def node_consolidated: Boolean = state.node_consolidated(version, node_name) - val commands_loading: List[Command] = if (node_name.is_theory) Nil else version.nodes.commands_loading(node_name) diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Tue May 29 20:01:50 2018 +0200 +++ b/src/Pure/PIDE/markup.ML Tue May 29 22:29:32 2018 +0200 @@ -167,6 +167,7 @@ val runningN: string val running: T val finishedN: string val finished: T val failedN: string val failed: T + val initializedN: string val initialized: T val consolidatedN: string val consolidated: T val exec_idN: string val initN: string @@ -580,6 +581,8 @@ val (runningN, running) = markup_elem "running"; val (finishedN, finished) = markup_elem "finished"; val (failedN, failed) = markup_elem "failed"; + +val (initializedN, initialized) = markup_elem "initialized"; val (consolidatedN, consolidated) = markup_elem "consolidated"; diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Tue May 29 20:01:50 2018 +0200 +++ b/src/Pure/PIDE/markup.scala Tue May 29 22:29:32 2018 +0200 @@ -426,6 +426,8 @@ val RUNNING = "running" val FINISHED = "finished" val FAILED = "failed" + + val INITIALIZED = "initialized" val CONSOLIDATED = "consolidated" diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Tue May 29 20:01:50 2018 +0200 +++ b/src/Pure/PIDE/protocol.scala Tue May 29 22:29:32 2018 +0200 @@ -142,7 +142,8 @@ /* node status */ sealed case class Node_Status( - unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, consolidated: Boolean) + unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, + initialized: Boolean, consolidated: Boolean) { def ok: Boolean = failed == 0 def total: Int = unprocessed + running + warned + failed + finished @@ -150,15 +151,16 @@ def json: JSON.Object.T = JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed, "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished, - "consolidated" -> consolidated) + "initialized" -> initialized, "consolidated" -> consolidated) } def node_status( state: Document.State, version: Document.Version, - name: Document.Node.Name, - node: Document.Node): Node_Status = + name: Document.Node.Name): Node_Status = { + val node = version.nodes(name) + var unprocessed = 0 var running = 0 var warned = 0 @@ -174,9 +176,10 @@ else if (status.is_finished) finished += 1 else unprocessed += 1 } + val initialized = state.node_initialized(version, name) val consolidated = state.node_consolidated(version, name) - Node_Status(unprocessed, running, warned, failed, finished, consolidated) + Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated) } diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Tue May 29 20:01:50 2018 +0200 +++ b/src/Pure/PIDE/resources.scala Tue May 29 22:29:32 2018 +0200 @@ -300,7 +300,7 @@ private def require_thy( progress: Progress, initiators: List[Document.Node.Name], - required: Dependencies, + dependencies: Dependencies, thy: (Document.Node.Name, Position.T)): Dependencies = { val (name, pos) = thy @@ -309,10 +309,10 @@ "The error(s) above occurred for theory " + quote(name.theory) + required_by(initiators) + Position.here(pos) - if (required.seen(name)) required + if (dependencies.seen(name)) dependencies else { - val required1 = required + name - if (session_base.loaded_theory(name)) required1 + val dependencies1 = dependencies + name + if (session_base.loaded_theory(name)) dependencies1 else { try { if (initiators.contains(name)) error(cycle_msg(initiators)) @@ -322,11 +322,11 @@ try { check_thy(name, Token.Pos.file(name.node)).cat_errors(message) } catch { case ERROR(msg) => cat_error(msg, message) } Document.Node.Entry(name, header) :: - require_thys(progress, name :: initiators, required1, header.imports) + require_thys(progress, name :: initiators, dependencies1, header.imports) } catch { case e: Throwable => - Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1 + Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: dependencies1 } } } @@ -335,9 +335,9 @@ private def require_thys( progress: Progress, initiators: List[Document.Node.Name], - required: Dependencies, + dependencies: Dependencies, thys: List[(Document.Node.Name, Position.T)]): Dependencies = - (required /: thys)(require_thy(progress, initiators, _, _)) + (dependencies /: thys)(require_thy(progress, initiators, _, _)) def dependencies( thys: List[(Document.Node.Name, Position.T)], diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Tue May 29 20:01:50 2018 +0200 +++ b/src/Pure/Thy/export.scala Tue May 29 22:29:32 2018 +0200 @@ -251,7 +251,7 @@ Usage: isabelle export [OPTIONS] SESSION Options are: - -D DIR target directory for exported files (default: """ + default_export_dir + """) + -O DIR output directory for exported files (default: """ + default_export_dir + """) -d DIR include session directory -l list exports -n no build of session @@ -266,7 +266,7 @@ (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc], and variants {pattern1,pattern2,pattern3}. """, - "D:" -> (arg => export_dir = Path.explode(arg)), + "O:" -> (arg => export_dir = Path.explode(arg)), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "l" -> (_ => export_list = true), "n" -> (_ => no_build = true), diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue May 29 20:01:50 2018 +0200 +++ b/src/Pure/Thy/sessions.scala Tue May 29 22:29:32 2018 +0200 @@ -146,6 +146,7 @@ doc_names: List[String] = Nil, global_theories: Map[String, String] = Map.empty, loaded_theories: Graph[String, Outer_Syntax] = Graph.string, + used_theories: List[Document.Node.Name] = Nil, known: Known = Known.empty, overall_syntax: Outer_Syntax = Outer_Syntax.empty, imported_sources: List[(Path, SHA1.Digest)] = Nil, @@ -349,6 +350,7 @@ doc_names = doc_names, global_theories = global_theories, loaded_theories = dependencies.loaded_theories, + used_theories = dependencies.theories, known = known, overall_syntax = overall_syntax, imported_sources = check_sources(imported_files), diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Pure/Thy/thy_resources.scala --- a/src/Pure/Thy/thy_resources.scala Tue May 29 20:01:50 2018 +0200 +++ b/src/Pure/Thy/thy_resources.scala Tue May 29 22:29:32 2018 +0200 @@ -60,6 +60,7 @@ val version: Document.Version, val nodes: List[(Document.Node.Name, Protocol.Node_Status)]) { + def node_names: List[Document.Node.Name] = nodes.map(_._1) def ok: Boolean = nodes.forall({ case (_, st) => st.ok }) def messages(node_name: Document.Node.Name): List[(XML.Tree, Position.T)] = @@ -73,6 +74,13 @@ } yield (tree, pos)).toList } + def markup_to_XML(node_name: Document.Node.Name, + range: Text.Range = Text.Range.full, + elements: Markup.Elements = Markup.Elements.full): XML.Body = + { + state.markup_to_XML(version, node_name, range, elements) + } + def exports(node_name: Document.Node.Name): List[Export.Entry] = { val node = version.nodes(node_name) @@ -125,7 +133,7 @@ case Some(version) if dep_theories.forall(state.node_consolidated(version, _)) => val nodes = for (name <- dep_theories) - yield (name -> Protocol.node_status(state, version, name, version.nodes(name))) + yield (name -> Protocol.node_status(state, version, name)) try { result.fulfill(Theories_Result(state, version, nodes)) } catch { case _: IllegalStateException => } case _ => diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Tue May 29 20:01:50 2018 +0200 +++ b/src/Pure/Tools/dump.scala Tue May 29 22:29:32 2018 +0200 @@ -9,12 +9,67 @@ object Dump { + /* aspects */ + + sealed case class Aspect_Args( + options: Options, progress: Progress, output_dir: Path, result: Thy_Resources.Theories_Result) + { + def write(node_name: Document.Node.Name, file_name: String, bytes: Bytes) + { + val path = output_dir + Path.basic(node_name.theory) + Path.basic(file_name) + Isabelle_System.mkdirs(path.dir) + Bytes.write(path, bytes) + } + + def write(node_name: Document.Node.Name, file_name: String, text: String) + { + write(node_name, file_name, Bytes(text)) + } + } + + sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit) + + private val known_aspects = + List( + Aspect("list", "list theory nodes", + { case args => + for (node_name <- args.result.node_names) args.progress.echo(node_name.toString) + }), + Aspect("messages", "output messages (YXML format)", + { case args => + for (node_name <- args.result.node_names) { + args.write(node_name, "messages.yxml", + YXML.string_of_body(args.result.messages(node_name).iterator.map(_._1).toList)) + } + }), + Aspect("markup", "PIDE markup (YXML format)", + { case args => + for (node_name <- args.result.node_names) { + args.write(node_name, "markup.yxml", + YXML.string_of_body(args.result.markup_to_XML(node_name))) + } + }) + ) + + def show_aspects: String = + cat_lines(known_aspects.sortBy(_.name).map(aspect => aspect.name + " - " + aspect.description)) + + def the_aspect(name: String): Aspect = + known_aspects.find(aspect => aspect.name == name) getOrElse + error("Unknown aspect " + quote(name)) + + + /* dump */ + + val default_output_dir = Path.explode("dump") + def dump(options: Options, logic: String, - consume: Thy_Resources.Theories_Result => Unit = _ => (), + aspects: List[Aspect] = Nil, progress: Progress = No_Progress, log: Logger = No_Logger, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, + output_dir: Path = default_output_dir, verbose: Boolean = false, system_mode: Boolean = false, selection: Sessions.Selection = Sessions.Selection.empty): Process_Result = @@ -24,22 +79,37 @@ val dump_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", false) + + /* dependencies */ + val deps = Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs). selection_deps(selection) + val include_sessions = + deps.sessions_structure.imports_topological_order + + val use_theories = + deps.sessions_structure.build_topological_order. + flatMap(session_name => deps.session_bases(session_name).used_theories.map(_.theory)) + + + /* session */ + val session = Thy_Resources.start_session(dump_options, logic, session_dirs = dirs, - include_sessions = deps.sessions_structure.imports_topological_order, - progress = progress, log = log) + include_sessions = include_sessions, progress = progress, log = log) + + val theories_result = session.use_theories(use_theories, progress = progress) + val session_result = session.stop() + - val theories = deps.all_known.theory_graph.topological_order.map(_.theory) - val theories_result = session.use_theories(theories, progress = progress) + /* dump aspects */ - try { consume(theories_result) } - catch { case exn: Throwable => session.stop (); throw exn } + val aspect_args = Aspect_Args(dump_options, progress, output_dir, theories_result) + aspects.foreach(_.operation(aspect_args)) - session.stop() + session_result } @@ -48,8 +118,10 @@ val isabelle_tool = Isabelle_Tool("dump", "dump build database produced by PIDE session.", args => { + var aspects: List[Aspect] = Nil var base_sessions: List[String] = Nil var select_dirs: List[Path] = Nil + var output_dir = default_output_dir var requirements = false var exclude_session_groups: List[String] = Nil var all_sessions = false @@ -65,8 +137,10 @@ Usage: isabelle dump [OPTIONS] [SESSIONS ...] Options are: + -A NAMES dump named aspects (comma-separated list, see below) -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions + -O DIR output directory for dumped files (default: """ + default_output_dir + """) -R operate on requirements of selected sessions -X NAME exclude sessions from group NAME and all descendants -a select all sessions @@ -78,9 +152,14 @@ -v verbose -x NAME exclude session NAME and all descendants - Dump build database (PIDE markup etc.) based on dynamic session.""", + Dump build database produced by PIDE session. The following dump aspects + are known (option -A): + +""" + Library.prefix_lines(" ", show_aspects) + "\n", + "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect(_))), "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), + "O:" -> (arg => output_dir = Path.explode(arg)), "R" -> (_ => requirements = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), "a" -> (_ => all_sessions = true), @@ -96,18 +175,13 @@ val progress = new Console_Progress(verbose = verbose) - def consume(theories_result: Thy_Resources.Theories_Result) - { - // FIXME - for ((node, _) <- theories_result.nodes) progress.echo(node.toString) - } - val result = dump(options, logic, - consume = consume _, + aspects = aspects, progress = progress, dirs = dirs, select_dirs = select_dirs, + output_dir = output_dir, verbose = verbose, selection = Sessions.Selection( requirements = requirements, diff -r 56c57e91edf9 -r 88c07fabd5b4 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Tue May 29 20:01:50 2018 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Tue May 29 22:29:32 2018 +0200 @@ -228,21 +228,17 @@ val snapshot = PIDE.session.snapshot() val nodes = snapshot.version.nodes - val iterator = - restriction match { - case Some(names) => names.iterator.map(name => (name, nodes(name))) - case None => nodes.iterator - } val nodes_status1 = - (nodes_status /: iterator)({ case (status, (name, node)) => - if (PIDE.resources.is_hidden(name) || - PIDE.resources.session_base.loaded_theory(name) || - node.is_empty) status - else { - val st = Protocol.node_status(snapshot.state, snapshot.version, name, node) - status + (name -> st) - } - }) + (nodes_status /: (restriction.getOrElse(nodes.domain).iterator))( + { case (status, name) => + if (PIDE.resources.is_hidden(name) || + PIDE.resources.session_base.loaded_theory(name) || + nodes(name).is_empty) status + else { + val st = Protocol.node_status(snapshot.state, snapshot.version, name) + status + (name -> st) + } + }) val nodes_status2 = nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_suppressed(_))