--- 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)
--- 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))
})
}
--- 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 *)
--- 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 */
--- 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] =
--- 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,
--- 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 =
--- 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 =
--- /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))
+ }
+ })
+}
--- 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
--- 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 */