# HG changeset patch # User wenzelm # Date 1546291294 -3600 # Node ID 8fd576a99a5949839b92ba668abb9da7cb58b943 # Parent b07ccc6fb13f862819c10bca56cd0471c1eecd6e# Parent 636b3c03a61af6bd04a1b70cd8c81ffec7f92475 merged diff -r b07ccc6fb13f -r 8fd576a99a59 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Mon Dec 31 13:24:20 2018 +0100 +++ b/src/Pure/PIDE/document.scala Mon Dec 31 22:21:34 2018 +0100 @@ -293,6 +293,11 @@ def has_header: Boolean = header != Node.no_header + override def toString: String = + if (is_empty) "empty" + else if (get_blob.isDefined) "blob" + else "node" + def commands: Linear_Set[Command] = _commands.commands def load_commands: List[Command] = _commands.load_commands def load_commands_changed(doc_blobs: Blobs): Boolean = @@ -528,6 +533,7 @@ def node_name: Node.Name def node: Node + def nodes: List[(Node.Name, Node)] def commands_loading: List[Command] def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] @@ -1024,6 +1030,10 @@ val node_name: Node.Name = name val node: Node = version.nodes(name) + def nodes: List[(Node.Name, Node)] = + (node_name :: node.load_commands.flatMap(_.blobs_names)). + map(name => (name, version.nodes(name))) + val commands_loading: List[Command] = if (node_name.is_theory) Nil else version.nodes.commands_loading(node_name) diff -r b07ccc6fb13f -r 8fd576a99a59 src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Mon Dec 31 13:24:20 2018 +0100 +++ b/src/Pure/PIDE/headless.scala Mon Dec 31 22:21:34 2018 +0100 @@ -10,6 +10,7 @@ import java.io.{File => JFile} import scala.annotation.tailrec +import scala.collection.mutable object Headless @@ -161,13 +162,17 @@ commit_cleanup_delay: Time = default_commit_cleanup_delay, progress: Progress = No_Progress): Use_Theories_Result = { - val dep_theories = + val dependencies = { val import_names = theories.map(thy => resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none) - resources.dependencies(import_names, progress = progress).check_errors.theories + resources.dependencies(import_names, progress = progress).check_errors } + val dep_theories = dependencies.theories + val dep_files = + dependencies.loaded_files(false).flatMap(_._2). + map(path => Document.Node.Name(resources.append("", path))) val use_theories_state = Synchronized(Use_Theories_State()) @@ -258,7 +263,7 @@ try { session.commands_changed += consumer - resources.load_theories(session, id, dep_theories, progress) + resources.load_theories(session, id, dep_theories, dep_files, progress) use_theories_state.value.await_result check_progress.cancel } @@ -341,9 +346,51 @@ } sealed case class State( - required: Multi_Map[Document.Node.Name, UUID.T] = Multi_Map.empty, - theories: Map[Document.Node.Name, Theory] = Map.empty) + blobs: Map[Document.Node.Name, Document.Blob] = Map.empty, + theories: Map[Document.Node.Name, Theory] = Map.empty, + required: Multi_Map[Document.Node.Name, UUID.T] = Multi_Map.empty) { + /* blobs */ + + def doc_blobs: Document.Blobs = Document.Blobs(blobs) + + def update_blobs(names: List[Document.Node.Name]): (Document.Blobs, State) = + { + val new_blobs = + names.flatMap(name => + { + val bytes = Bytes.read(name.path) + def new_blob: Document.Blob = + { + val text = bytes.text + Document.Blob(bytes, text, Symbol.Text_Chunk(text), changed = true) + } + blobs.get(name) match { + case Some(blob) => if (blob.bytes == bytes) None else Some(name -> new_blob) + case None => Some(name -> new_blob) + } + }) + val blobs1 = (blobs /: new_blobs)(_ + _) + val blobs2 = (blobs /: new_blobs)({ case (map, (a, b)) => map + (a -> b.unchanged) }) + (Document.Blobs(blobs1), copy(blobs = blobs2)) + } + + def blob_edits(name: Document.Node.Name, old_blob: Option[Document.Blob]) + : List[Document.Edit_Text] = + { + val blob = blobs.getOrElse(name, error("Missing blob " + quote(name.toString))) + val text_edits = + old_blob match { + case None => List(Text.Edit.insert(0, blob.source)) + case Some(blob0) => Text.Edit.replace(0, blob0.source, blob.source) + } + if (text_edits.isEmpty) Nil + else List(name -> Document.Node.Blob(blob), name -> Document.Node.Edits(text_edits)) + } + + + /* theories */ + lazy val theory_graph: Graph[Document.Node.Name, Unit] = { val entries = @@ -389,7 +436,7 @@ val edits = theory1.node_edits(Some(theory)) (edits, (node_name, theory1)) } - session.update(Document.Blobs.empty, theory_edits.flatMap(_._1)) + session.update(doc_blobs, theory_edits.flatMap(_._1)) st1.update_theories(theory_edits.map(_._2)) } @@ -403,7 +450,7 @@ val (retained, purged) = all_nodes.partition(retain) val purge_edits = purged.flatMap(name => theories(name).purge_edits) - session.update(Document.Blobs.empty, purge_edits) + session.update(doc_blobs, purge_edits) ((purged, retained), remove_theories(purged)) } @@ -475,6 +522,7 @@ session: Session, id: UUID.T, dep_theories: List[Document.Node.Name], + dep_files: List[Document.Node.Name], progress: Progress) { val loaded_theories = @@ -494,7 +542,7 @@ state.change(st => { - val st1 = st.insert_required(id, dep_theories) + val (doc_blobs1, st1) = st.insert_required(id, dep_theories).update_blobs(dep_files) val theory_edits = for (theory <- loaded_theories) yield { @@ -503,7 +551,11 @@ val edits = theory1.node_edits(st1.theories.get(node_name)) (edits, (node_name, theory1)) } - session.update(Document.Blobs.empty, theory_edits.flatMap(_._1)) + val file_edits = + for { node_name <- dep_files if doc_blobs1.changed(node_name) } + yield st1.blob_edits(node_name, st.blobs.get(node_name)) + + session.update(doc_blobs1, theory_edits.flatMap(_._1) ::: file_edits.flatten) st1.update_theories(theory_edits.map(_._2)) }) } diff -r b07ccc6fb13f -r 8fd576a99a59 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Mon Dec 31 13:24:20 2018 +0100 +++ b/src/Pure/PIDE/markup.ML Mon Dec 31 22:21:34 2018 +0100 @@ -45,6 +45,7 @@ val refN: string val completionN: string val completion: T val no_completionN: string val no_completion: T + val updateN: string val update: T val lineN: string val end_lineN: string val offsetN: string @@ -336,6 +337,8 @@ val (completionN, completion) = markup_elem "completion"; val (no_completionN, no_completion) = markup_elem "no_completion"; +val (updateN, update) = markup_elem "update"; + (* position *) diff -r b07ccc6fb13f -r 8fd576a99a59 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Mon Dec 31 13:24:20 2018 +0100 +++ b/src/Pure/PIDE/markup.scala Mon Dec 31 22:21:34 2018 +0100 @@ -115,6 +115,8 @@ val COMPLETION = "completion" val NO_COMPLETION = "no_completion" + val UPDATE = "update" + /* position */ diff -r b07ccc6fb13f -r 8fd576a99a59 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Mon Dec 31 13:24:20 2018 +0100 +++ b/src/Pure/PIDE/resources.scala Mon Dec 31 22:21:34 2018 +0100 @@ -90,11 +90,12 @@ } } - def pure_files(syntax: Outer_Syntax, dir: Path): List[Path] = + def pure_files(syntax: Outer_Syntax): List[Path] = { + val pure_dir = Path.explode("~~/src/Pure") val roots = for { (name, _) <- Thy_Header.ml_roots } - yield (dir + Path.explode(name)).expand + yield (pure_dir + Path.explode(name)).expand val files = for { (path, (_, theory)) <- roots zip Thy_Header.ml_roots @@ -344,11 +345,20 @@ graph2.map_node(name, _ => syntax) }) - def loaded_files: List[(String, List[Path])] = + def loaded_files(pure: Boolean): List[(String, List[Path])] = { - theories.map(_.theory) zip - Par_List.map((e: () => List[Path]) => e(), - theories.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name))) + val loaded_files = + theories.map(_.theory) zip + Par_List.map((e: () => List[Path]) => e(), + theories.map(name => + resources.loaded_files(loaded_theories.get_node(name.theory), name))) + + if (pure) { + val pure_files = resources.pure_files(overall_syntax) + loaded_files.map({ case (name, files) => + (name, if (name == Thy_Header.PURE) pure_files ::: files else files) }) + } + else loaded_files } def imported_files: List[Path] = diff -r b07ccc6fb13f -r 8fd576a99a59 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Mon Dec 31 13:24:20 2018 +0100 +++ b/src/Pure/System/isabelle_tool.scala Mon Dec 31 22:21:34 2018 +0100 @@ -155,6 +155,7 @@ Present.isabelle_tool, Profiling_Report.isabelle_tool, Server.isabelle_tool, + Update.isabelle_tool, Update_Cartouches.isabelle_tool, Update_Comments.isabelle_tool, Update_Header.isabelle_tool, diff -r b07ccc6fb13f -r 8fd576a99a59 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Mon Dec 31 13:24:20 2018 +0100 +++ b/src/Pure/Thy/sessions.scala Mon Dec 31 22:21:34 2018 +0100 @@ -303,14 +303,7 @@ val theory_files = dependencies.theories.map(_.path) val loaded_files = - if (inlined_files) { - if (Sessions.is_pure(info.name)) { - val pure_files = resources.pure_files(overall_syntax, info.dir) - dependencies.loaded_files.map({ case (name, files) => - (name, if (name == Thy_Header.PURE) pure_files ::: files else files) }) - } - else dependencies.loaded_files - } + if (inlined_files) dependencies.loaded_files(Sessions.is_pure(info.name)) else Nil val session_files = diff -r b07ccc6fb13f -r 8fd576a99a59 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Mon Dec 31 13:24:20 2018 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Mon Dec 31 22:21:34 2018 +0100 @@ -301,7 +301,7 @@ { val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits) - def get_blob(name: Document.Node.Name) = + def get_blob(name: Document.Node.Name): Option[Document.Blob] = doc_blobs.get(name) orElse previous.nodes(name).get_blob def can_import(name: Document.Node.Name): Boolean = diff -r b07ccc6fb13f -r 8fd576a99a59 src/Pure/Tools/update.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/update.scala Mon Dec 31 22:21:34 2018 +0100 @@ -0,0 +1,132 @@ +/* Title: Pure/Tools/update.scala + Author: Makarius + +Update theory sources based on PIDE markup. +*/ + +package isabelle + + +object Update +{ + def update(options: Options, logic: String, + progress: Progress = No_Progress, + log: Logger = No_Logger, + dirs: List[Path] = Nil, + select_dirs: List[Path] = Nil, + system_mode: Boolean = false, + selection: Sessions.Selection = Sessions.Selection.empty) + { + Build.build_logic(options, logic, build_heap = true, progress = progress, + dirs = dirs ::: select_dirs, system_mode = system_mode, strict = true) + + val dump_options = Dump.make_options(options) + + val deps = + Dump.dependencies(dump_options, progress = progress, + dirs = dirs, select_dirs = select_dirs, selection = selection)._1 + + val resources = + Headless.Resources.make(dump_options, logic, progress = progress, log = log, + session_dirs = dirs ::: select_dirs, + include_sessions = deps.sessions_structure.imports_topological_order) + + def update_xml(xml: XML.Body): XML.Body = + xml flatMap { + case XML.Wrapped_Elem(markup, body1, body2) => + if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2) + case XML.Elem(_, body) => update_xml(body) + case t => List(t) + } + + Dump.session(deps, resources, progress = progress, + process_theory = + (deps: Sessions.Deps, snapshot: Document.Snapshot, status: Document_Status.Node_Status) => + { + for ((node_name, node) <- snapshot.nodes) { + val xml = + snapshot.state.markup_to_XML(snapshot.version, node_name, + Text.Range.full, Markup.Elements(Markup.UPDATE)) + + val source1 = Symbol.encode(XML.content(update_xml(xml))) + if (source1 != Symbol.encode(node.source)) { + progress.echo("Updating " + node_name.path) + File.write(node_name.path, source1) + } + } + }) + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = + Isabelle_Tool("update", "update theory sources based on PIDE markup", args => + { + var base_sessions: List[String] = Nil + var select_dirs: List[Path] = Nil + var requirements = false + var exclude_session_groups: List[String] = Nil + var all_sessions = false + var dirs: List[Path] = Nil + var session_groups: List[String] = Nil + var logic = Isabelle_System.getenv("ISABELLE_LOGIC") + var options = Options.init() + var system_mode = false + var verbose = false + var exclude_sessions: List[String] = Nil + + val getopts = Getopts(""" +Usage: isabelle update [OPTIONS] [SESSIONS ...] + + Options are: + -B NAME include session NAME and all descendants + -D DIR include session directory and select its sessions + -R operate on requirements of selected sessions + -X NAME exclude sessions from group NAME and all descendants + -a select all sessions + -d DIR include session directory + -g NAME select session group NAME + -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -s system build mode for logic image + -u OPT overide update option: shortcut for "-o update_OPT" + -v verbose + -x NAME exclude session NAME and all descendants + + Update theory sources based on PIDE markup. +""", + "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), + "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), + "R" -> (_ => requirements = true), + "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), + "a" -> (_ => all_sessions = true), + "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), + "g:" -> (arg => session_groups = session_groups ::: List(arg)), + "l:" -> (arg => logic = arg), + "o:" -> (arg => options = options + arg), + "s" -> (_ => system_mode = true), + "u:" -> (arg => options = options + ("update_" + arg)), + "v" -> (_ => verbose = true), + "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) + + val sessions = getopts(args) + + val progress = new Console_Progress(verbose = verbose) + + progress.interrupt_handler { + update(options, logic, + progress = progress, + dirs = dirs, + select_dirs = select_dirs, + selection = Sessions.Selection( + requirements = requirements, + all_sessions = all_sessions, + base_sessions = base_sessions, + exclude_session_groups = exclude_session_groups, + exclude_sessions = exclude_sessions, + session_groups = session_groups, + sessions = sessions)) + } + }) +} diff -r b07ccc6fb13f -r 8fd576a99a59 src/Pure/build-jars --- a/src/Pure/build-jars Mon Dec 31 13:24:20 2018 +0100 +++ b/src/Pure/build-jars Mon Dec 31 22:21:34 2018 +0100 @@ -160,6 +160,7 @@ Tools/simplifier_trace.scala Tools/spell_checker.scala Tools/task_statistics.scala + Tools/update.scala Tools/update_cartouches.scala Tools/update_comments.scala Tools/update_header.scala diff -r b07ccc6fb13f -r 8fd576a99a59 src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Mon Dec 31 13:24:20 2018 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Mon Dec 31 22:21:34 2018 +0100 @@ -144,7 +144,7 @@ def get_blob: Option[Document.Blob] = if (is_theory) None - else Some((Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))) + else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty)) /* bibtex entries */