diff --git a/src/Pure/General/graph.scala b/src/Pure/General/graph.scala --- a/src/Pure/General/graph.scala +++ b/src/Pure/General/graph.scala @@ -1,330 +1,334 @@ /* Title: Pure/General/graph.scala Author: Makarius Directed graphs. */ package isabelle import scala.collection.immutable.{SortedMap, SortedSet} import scala.annotation.tailrec object Graph { class Duplicate[Key](val key: Key) extends Exception { override def toString: String = "Graph.Duplicate(" + key.toString + ")" } class Undefined[Key](val key: Key) extends Exception { override def toString: String = "Graph.Undefined(" + key.toString + ")" } class Cycles[Key](val cycles: List[List[Key]]) extends Exception { override def toString: String = cycles.mkString("Graph.Cycles(", ",\n", ")") } def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] = new Graph[Key, A](SortedMap.empty(ord)) def make[Key, A](entries: List[((Key, A), List[Key])], symmetric: Boolean = false)(implicit ord: Ordering[Key]): Graph[Key, A] = { val graph1 = (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) } val graph2 = (graph1 /: entries) { case (graph, ((x, _), ys)) => (graph /: ys)({ case (g, y) => if (symmetric) g.add_edge(y, x) else g.add_edge(x, y) }) } graph2 } def string[A]: Graph[String, A] = empty(Ordering.String) def int[A]: Graph[Int, A] = empty(Ordering.Int) def long[A]: Graph[Long, A] = empty(Ordering.Long) /* XML data representation */ def encode[Key, A](key: XML.Encode.T[Key], info: XML.Encode.T[A]): XML.Encode.T[Graph[Key, A]] = (graph: Graph[Key, A]) => { import XML.Encode._ list(pair(pair(key, info), list(key)))(graph.dest) } def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A])( implicit ord: Ordering[Key]): XML.Decode.T[Graph[Key, A]] = (body: XML.Body) => { import XML.Decode._ make(list(pair(pair(key, info), list(key)))(body))(ord) } } final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))]) { type Keys = SortedSet[Key] type Entry = (A, (Keys, Keys)) def ordering: Ordering[Key] = rep.ordering def empty_keys: Keys = SortedSet.empty[Key](ordering) /* graphs */ def is_empty: Boolean = rep.isEmpty def defined(x: Key): Boolean = rep.isDefinedAt(x) def domain: Set[Key] = rep.keySet def size: Int = rep.size def iterator: Iterator[(Key, Entry)] = rep.iterator def keys_iterator: Iterator[Key] = iterator.map(_._1) def keys: List[Key] = keys_iterator.toList def dest: List[((Key, A), List[Key])] = (for ((x, (i, (_, succs))) <- iterator) yield ((x, i), succs.toList)).toList override def toString: String = dest.map({ case ((x, _), ys) => x.toString + " -> " + ys.iterator.map(_.toString).mkString("{", ", ", "}") }) .mkString("Graph(", ", ", ")") private def get_entry(x: Key): Entry = rep.get(x) match { case Some(entry) => entry case None => throw new Graph.Undefined(x) } private def map_entry(x: Key, f: Entry => Entry): Graph[Key, A] = new Graph[Key, A](rep + (x -> f(get_entry(x)))) /* nodes */ def get_node(x: Key): A = get_entry(x)._1 def map_node(x: Key, f: A => A): Graph[Key, A] = map_entry(x, { case (i, ps) => (f(i), ps) }) /* reachability */ /*reachable nodes with length of longest path*/ def reachable_length( count: Key => Long, next: Key => Keys, xs: List[Key]): Map[Key, Long] = { def reach(length: Long)(rs: Map[Key, Long], x: Key): Map[Key, Long] = if (rs.get(x) match { case Some(n) => n >= length case None => false }) rs else ((rs + (x -> length)) /: next(x))(reach(length + count(x))) (Map.empty[Key, Long] /: xs)(reach(0)) } def node_height(count: Key => Long): Map[Key, Long] = reachable_length(count, imm_preds, maximals) def node_depth(count: Key => Long): Map[Key, Long] = reachable_length(count, imm_succs, minimals) /*reachable nodes with size limit*/ def reachable_limit( limit: Long, count: Key => Long, next: Key => Keys, xs: List[Key]): Keys = { def reach(res: (Long, Keys), x: Key): (Long, Keys) = { val (n, rs) = res if (rs.contains(x)) res else ((n + count(x), rs + x) /: next(x))(reach) } @tailrec def reachs(size: Long, rs: Keys, rest: List[Key]): Keys = rest match { case Nil => rs case head :: tail => val (size1, rs1) = reach((size, rs), head) if (size > 0 && size1 > limit) rs else reachs(size1, rs1, tail) } reachs(0, empty_keys, xs) } /*reachable nodes with result in topological order (for acyclic graphs)*/ - def reachable(next: Key => Keys, xs: List[Key]): (List[List[Key]], Keys) = + private def reachable(next: Key => Keys, xs: List[Key], rev: Boolean = false): (List[List[Key]], Keys) = { def reach(x: Key, reached: (List[Key], Keys)): (List[Key], Keys) = { val (rs, r_set) = reached if (r_set(x)) reached else { - val (rs1, r_set1) = (next(x) :\ (rs, r_set + x))(reach) + val (rs1, r_set1) = + if (rev) ((rs, r_set + x) /: next(x))({ case (b, a) => reach(a, b) }) + else (next(x) :\ (rs, r_set + x))(reach) (x :: rs1, r_set1) } } def reachs(reached: (List[List[Key]], Keys), x: Key): (List[List[Key]], Keys) = { val (rss, r_set) = reached val (rs, r_set1) = reach(x, (Nil, r_set)) (rs :: rss, r_set1) } ((List.empty[List[Key]], empty_keys) /: xs)(reachs) } /*immediate*/ def imm_preds(x: Key): Keys = get_entry(x)._2._1 def imm_succs(x: Key): Keys = get_entry(x)._2._2 /*transitive*/ + def all_preds_rev(xs: List[Key]): List[Key] = + reachable(imm_preds, xs, rev = true)._1.flatten.reverse def all_preds(xs: List[Key]): List[Key] = reachable(imm_preds, xs)._1.flatten def all_succs(xs: List[Key]): List[Key] = reachable(imm_succs, xs)._1.flatten /*strongly connected components; see: David King and John Launchbury, "Structuring Depth First Search Algorithms in Haskell"*/ def strong_conn: List[List[Key]] = reachable(imm_preds, all_succs(keys))._1.filterNot(_.isEmpty).reverse /* minimal and maximal elements */ def minimals: List[Key] = (List.empty[Key] /: rep) { case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms } def maximals: List[Key] = (List.empty[Key] /: rep) { case (ms, (m, (_, (_, succs)))) => if (succs.isEmpty) m :: ms else ms } def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty def is_isolated(x: Key): Boolean = is_minimal(x) && is_maximal(x) /* node operations */ def new_node(x: Key, info: A): Graph[Key, A] = { if (defined(x)) throw new Graph.Duplicate(x) else new Graph[Key, A](rep + (x -> (info, (empty_keys, empty_keys)))) } def default_node(x: Key, info: A): Graph[Key, A] = if (defined(x)) this else new_node(x, info) private def del_adjacent(fst: Boolean, x: Key)(map: SortedMap[Key, Entry], y: Key) : SortedMap[Key, Entry] = map.get(y) match { case None => map case Some((i, (preds, succs))) => map + (y -> (i, if (fst) (preds - x, succs) else (preds, succs - x))) } def del_node(x: Key): Graph[Key, A] = { val (preds, succs) = get_entry(x)._2 new Graph[Key, A]( (((rep - x) /: preds)(del_adjacent(false, x)) /: succs)(del_adjacent(true, x))) } def restrict(pred: Key => Boolean): Graph[Key, A] = (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph } def exclude(pred: Key => Boolean): Graph[Key, A] = restrict(name => !pred(name)) /* edge operations */ def edges_iterator: Iterator[(Key, Key)] = for { x <- keys_iterator; y <- imm_succs(x).iterator } yield (x, y) def is_edge(x: Key, y: Key): Boolean = defined(x) && defined(y) && imm_succs(x)(y) def add_edge(x: Key, y: Key): Graph[Key, A] = if (is_edge(x, y)) this else map_entry(y, { case (i, (preds, succs)) => (i, (preds + x, succs)) }). map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs + y)) }) def del_edge(x: Key, y: Key): Graph[Key, A] = if (is_edge(x, y)) map_entry(y, { case (i, (preds, succs)) => (i, (preds - x, succs)) }). map_entry(x, { case (i, (preds, succs)) => (i, (preds, succs - y)) }) else this /* irreducible paths -- Hasse diagram */ private def irreducible_preds(x_set: Keys, path: List[Key], z: Key): List[Key] = { def red(x: Key)(x1: Key) = is_edge(x, x1) && x1 != z @tailrec def irreds(xs0: List[Key], xs1: List[Key]): List[Key] = xs0 match { case Nil => xs1 case x :: xs => if (!x_set(x) || x == z || path.contains(x) || xs.exists(red(x)) || xs1.exists(red(x))) irreds(xs, xs1) else irreds(xs, x :: xs1) } irreds(imm_preds(z).toList, Nil) } def irreducible_paths(x: Key, y: Key): List[List[Key]] = { val (_, x_set) = reachable(imm_succs, List(x)) def paths(path: List[Key])(ps: List[List[Key]], z: Key): List[List[Key]] = if (x == z) (z :: path) :: ps else (ps /: irreducible_preds(x_set, path, z))(paths(z :: path)) if ((x == y) && !is_edge(x, x)) List(Nil) else paths(Nil)(Nil, y) } /* transitive closure and reduction */ private def transitive_step(z: Key): Graph[Key, A] = { val (preds, succs) = get_entry(z)._2 var graph = this for (x <- preds; y <- succs) graph = graph.add_edge(x, y) graph } def transitive_closure: Graph[Key, A] = (this /: keys_iterator)(_.transitive_step(_)) def transitive_reduction_acyclic: Graph[Key, A] = { val trans = this.transitive_closure if (trans.iterator.exists({ case (x, (_, (_, succs))) => succs.contains(x) })) error("Cyclic graph") var graph = this for { (x, (_, (_, succs))) <- iterator y <- succs if trans.imm_preds(y).exists(z => trans.is_edge(x, z)) } graph = graph.del_edge(x, y) graph } /* maintain acyclic graphs */ def add_edge_acyclic(x: Key, y: Key): Graph[Key, A] = if (is_edge(x, y)) this else { irreducible_paths(y, x) match { case Nil => add_edge(x, y) case cycles => throw new Graph.Cycles(cycles.map(x :: _)) } } def add_deps_acyclic(y: Key, xs: List[Key]): Graph[Key, A] = (this /: xs)(_.add_edge_acyclic(_, y)) def topological_order: List[Key] = all_succs(minimals) } diff --git a/src/Pure/PIDE/document.scala b/src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala +++ b/src/Pure/PIDE/document.scala @@ -1,1199 +1,1199 @@ /* Title: Pure/PIDE/document.scala Author: Makarius Document as collection of named nodes, each consisting of an editable list of commands, associated with asynchronous execution process. */ package isabelle import scala.collection.mutable object Document { /** document structure **/ /* overlays -- print functions with arguments */ object Overlays { val empty = new Overlays(Map.empty) } final class Overlays private(rep: Map[Node.Name, Node.Overlays]) { def apply(name: Node.Name): Node.Overlays = rep.getOrElse(name, Node.Overlays.empty) private def update(name: Node.Name, f: Node.Overlays => Node.Overlays): Overlays = { val node_overlays = f(apply(name)) new Overlays(if (node_overlays.is_empty) rep - name else rep + (name -> node_overlays)) } def insert(command: Command, fn: String, args: List[String]): Overlays = update(command.node_name, _.insert(command, fn, args)) def remove(command: Command, fn: String, args: List[String]): Overlays = update(command.node_name, _.remove(command, fn, args)) override def toString: String = rep.mkString("Overlays(", ",", ")") } /* document blobs: auxiliary files */ sealed case class Blob(bytes: Bytes, source: String, chunk: Symbol.Text_Chunk, changed: Boolean) { def unchanged: Blob = copy(changed = false) } object Blobs { def apply(blobs: Map[Node.Name, Blob]): Blobs = new Blobs(blobs) val empty: Blobs = apply(Map.empty) } final class Blobs private(blobs: Map[Node.Name, Blob]) { def get(name: Node.Name): Option[Blob] = blobs.get(name) def changed(name: Node.Name): Boolean = get(name) match { case Some(blob) => blob.changed case None => false } override def toString: String = blobs.mkString("Blobs(", ",", ")") } /* document nodes: theories and auxiliary files */ type Edit[A, B] = (Node.Name, Node.Edit[A, B]) type Edit_Text = Edit[Text.Edit, Text.Perspective] type Edit_Command = Edit[Command.Edit, Command.Perspective] object Node { /* header and name */ sealed case class Header( imports_pos: List[(Name, Position.T)] = Nil, keywords: Thy_Header.Keywords = Nil, abbrevs: Thy_Header.Abbrevs = Nil, errors: List[String] = Nil) { def imports: List[Name] = imports_pos.map(_._1) def append_errors(msgs: List[String]): Header = copy(errors = errors ::: msgs) def cat_errors(msg2: String): Header = copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2))) } val no_header: Header = Header() def bad_header(msg: String): Header = Header(errors = List(msg)) object Name { val empty: Name = Name("") object Ordering extends scala.math.Ordering[Name] { def compare(name1: Name, name2: Name): Int = name1.node compare name2.node } type Graph[A] = isabelle.Graph[Node.Name, A] def make_graph[A](entries: List[((Name, A), List[Name])]): Graph[A] = Graph.make(entries, symmetric = true)(Ordering) } sealed case class Name(node: String, master_dir: String = "", theory: String = "") { override def hashCode: Int = node.hashCode override def equals(that: Any): Boolean = that match { case other: Name => node == other.node case _ => false } def path: Path = Path.explode(File.standard_path(node)) def master_dir_path: Path = Path.explode(File.standard_path(master_dir)) def is_theory: Boolean = theory.nonEmpty def theory_base_name: String = Long_Name.base_name(theory) override def toString: String = if (is_theory) theory else node def map(f: String => String): Name = copy(f(node), f(master_dir), theory) def map_theory(f: String => String): Name = copy(node, master_dir, f(theory)) def json: JSON.Object.T = JSON.Object("node_name" -> node, "theory_name" -> theory) } sealed case class Entry(name: Node.Name, header: Node.Header) { def map(f: String => String): Entry = copy(name = name.map(f)) override def toString: String = name.toString } /* node overlays */ object Overlays { val empty = new Overlays(Multi_Map.empty) } final class Overlays private(rep: Multi_Map[Command, (String, List[String])]) { def commands: Set[Command] = rep.keySet def is_empty: Boolean = rep.isEmpty def dest: List[(Command, (String, List[String]))] = rep.iterator.toList def insert(cmd: Command, fn: String, args: List[String]): Overlays = new Overlays(rep.insert(cmd, (fn, args))) def remove(cmd: Command, fn: String, args: List[String]): Overlays = new Overlays(rep.remove(cmd, (fn, args))) override def toString: String = rep.mkString("Node.Overlays(", ",", ")") } /* edits */ sealed abstract class Edit[A, B] { def foreach(f: A => Unit) { this match { case Edits(es) => es.foreach(f) case _ => } } def is_void: Boolean = this match { case Edits(Nil) => true case _ => false } } case class Blob[A, B](blob: Document.Blob) extends Edit[A, B] case class Edits[A, B](edits: List[A]) extends Edit[A, B] case class Deps[A, B](header: Header) extends Edit[A, B] case class Perspective[A, B](required: Boolean, visible: B, overlays: Overlays) extends Edit[A, B] /* perspective */ type Perspective_Text = Perspective[Text.Edit, Text.Perspective] type Perspective_Command = Perspective[Command.Edit, Command.Perspective] val no_perspective_text: Perspective_Text = Perspective(false, Text.Perspective.empty, Overlays.empty) val no_perspective_command: Perspective_Command = Perspective(false, Command.Perspective.empty, Overlays.empty) def is_no_perspective_text(perspective: Perspective_Text): Boolean = !perspective.required && perspective.visible.is_empty && perspective.overlays.is_empty def is_no_perspective_command(perspective: Perspective_Command): Boolean = !perspective.required && perspective.visible.is_empty && perspective.overlays.is_empty /* commands */ object Commands { def apply(commands: Linear_Set[Command]): Commands = new Commands(commands) val empty: Commands = apply(Linear_Set.empty) def starts(commands: Iterator[Command], offset: Text.Offset = 0) : Iterator[(Command, Text.Offset)] = { var i = offset for (command <- commands) yield { val start = i i += command.length (command, start) } } def starts_pos(commands: Iterator[Command], pos: Token.Pos = Token.Pos.start) : Iterator[(Command, Token.Pos)] = { var p = pos for (command <- commands) yield { val start = p p = (p /: command.span.content)(_.advance(_)) (command, start) } } private val block_size = 256 } final class Commands private(val commands: Linear_Set[Command]) { lazy val load_commands: List[Command] = commands.iterator.filter(cmd => cmd.blobs.nonEmpty).toList private lazy val full_index: (Array[(Command, Text.Offset)], Text.Range) = { val blocks = new mutable.ListBuffer[(Command, Text.Offset)] var next_block = 0 var last_stop = 0 for ((command, start) <- Commands.starts(commands.iterator)) { last_stop = start + command.length while (last_stop + 1 > next_block) { blocks += (command -> start) next_block += Commands.block_size } } (blocks.toArray, Text.Range(0, last_stop)) } private def full_range: Text.Range = full_index._2 def iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = { if (commands.nonEmpty && full_range.contains(i)) { val (cmd0, start0) = full_index._1(i / Commands.block_size) Node.Commands.starts(commands.iterator(cmd0), start0) dropWhile { case (cmd, start) => start + cmd.length <= i } } else Iterator.empty } } val empty: Node = new Node() } final class Node private( val get_blob: Option[Document.Blob] = None, val header: Node.Header = Node.no_header, val syntax: Option[Outer_Syntax] = None, val text_perspective: Text.Perspective = Text.Perspective.empty, val perspective: Node.Perspective_Command = Node.no_perspective_command, _commands: Node.Commands = Node.Commands.empty) { def is_empty: Boolean = get_blob.isEmpty && header == Node.no_header && text_perspective.is_empty && Node.is_no_perspective_command(perspective) && commands.isEmpty 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 = load_commands.exists(_.blobs_changed(doc_blobs)) def init_blob(blob: Blob): Node = new Node(get_blob = Some(blob.unchanged)) def update_header(new_header: Node.Header): Node = new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands) def update_syntax(new_syntax: Option[Outer_Syntax]): Node = new Node(get_blob, header, new_syntax, text_perspective, perspective, _commands) def update_perspective( new_text_perspective: Text.Perspective, new_perspective: Node.Perspective_Command): Node = new Node(get_blob, header, syntax, new_text_perspective, new_perspective, _commands) def edit_perspective: Node.Edit[Text.Edit, Text.Perspective] = Node.Perspective(perspective.required, text_perspective, perspective.overlays) def same_perspective( other_text_perspective: Text.Perspective, other_perspective: Node.Perspective_Command): Boolean = text_perspective == other_text_perspective && perspective.required == other_perspective.required && perspective.visible.same(other_perspective.visible) && perspective.overlays == other_perspective.overlays def update_commands(new_commands: Linear_Set[Command]): Node = if (new_commands eq _commands.commands) this else new Node(get_blob, header, syntax, text_perspective, perspective, Node.Commands(new_commands)) def command_iterator(i: Text.Offset = 0): Iterator[(Command, Text.Offset)] = _commands.iterator(i) def command_iterator(range: Text.Range): Iterator[(Command, Text.Offset)] = command_iterator(range.start) takeWhile { case (_, start) => start < range.stop } def command_start(cmd: Command): Option[Text.Offset] = Node.Commands.starts(commands.iterator).find(_._1 == cmd).map(_._2) def source: String = get_blob match { case Some(blob) => blob.source case None => command_iterator(0).map({ case (cmd, _) => cmd.source }).mkString } } /* development graph */ object Nodes { val empty: Nodes = new Nodes(Graph.empty(Node.Name.Ordering)) } final class Nodes private(graph: Graph[Node.Name, Node]) { def apply(name: Node.Name): Node = graph.default_node(name, Node.empty).get_node(name) def is_suppressed(name: Node.Name): Boolean = { val graph1 = graph.default_node(name, Node.empty) graph1.is_maximal(name) && graph1.get_node(name).is_empty } def purge_suppressed: Option[Nodes] = graph.keys_iterator.filter(is_suppressed).toList match { case Nil => None case del => Some(new Nodes((graph /: del)(_.del_node(_)))) } def + (entry: (Node.Name, Node)): Nodes = { val (name, node) = entry val imports = node.header.imports val graph1 = (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty)) val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name)) val graph3 = (graph2 /: imports)((g, dep) => g.add_edge(dep, name)) 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) }) def theory_name(theory: String): Option[Node.Name] = graph.keys_iterator.find(name => name.theory == theory) def commands_loading(file_name: Node.Name): List[Command] = (for { (_, node) <- iterator cmd <- node.load_commands.iterator name <- cmd.blobs_names.iterator if name == file_name } yield cmd).toList def descendants(names: List[Node.Name]): List[Node.Name] = graph.all_succs(names) - def requirements(names: List[Node.Name]): List[Node.Name] = graph.all_preds(names).reverse + def requirements(names: List[Node.Name]): List[Node.Name] = graph.all_preds_rev(names) def topological_order: List[Node.Name] = graph.topological_order override def toString: String = topological_order.mkString("Nodes(", ",", ")") } /** versioning **/ /* particular document versions */ object Version { val init: Version = new Version() def make(nodes: Nodes): Version = new Version(Document_ID.make(), nodes) def purge_future(versions: Map[Document_ID.Version, Version], future: Future[Version]) : Future[Version] = { if (future.is_finished) { val version = future.join versions.get(version.id) match { case Some(version1) if !(version eq version1) => Future.value(version1) case _ => future } } else future } def purge_suppressed( versions: Map[Document_ID.Version, Version]): Map[Document_ID.Version, Version] = { (versions /: (for ((id, v) <- versions.iterator; v1 <- v.purge_suppressed) yield (id, v1)))(_ + _) } } final class Version private( val id: Document_ID.Version = Document_ID.none, val nodes: Nodes = Nodes.empty) { override def toString: String = "Version(" + id + ")" def purge_suppressed: Option[Version] = nodes.purge_suppressed.map(new Version(id, _)) } /* changes of plain text, eventually resulting in document edits */ object Change { val init: Change = new Change() def make(previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): Change = new Change(Some(previous), edits.reverse, version) } final class Change private( val previous: Option[Future[Version]] = Some(Future.value(Version.init)), val rev_edits: List[Edit_Text] = Nil, val version: Future[Version] = Future.value(Version.init)) { def is_finished: Boolean = (previous match { case None => true case Some(future) => future.is_finished }) && version.is_finished def truncate: Change = new Change(None, Nil, version) def purge(versions: Map[Document_ID.Version, Version]): Option[Change] = { val previous1 = previous.map(Version.purge_future(versions, _)) val version1 = Version.purge_future(versions, version) if ((previous eq previous1) && (version eq version1)) None else Some(new Change(previous1, rev_edits, version1)) } } /* history navigation */ object History { val init: History = new History() } final class History private( val undo_list: List[Change] = List(Change.init)) // non-empty list { override def toString: String = "History(" + undo_list.length + ")" def tip: Change = undo_list.head def + (change: Change): History = new History(change :: undo_list) def prune(check: Change => Boolean, retain: Int): Option[(List[Change], History)] = { val n = undo_list.iterator.zipWithIndex.find(p => check(p._1)).get._2 + 1 val (retained, dropped) = undo_list.splitAt(n max retain) retained.splitAt(retained.length - 1) match { case (prefix, List(last)) => Some(dropped, new History(prefix ::: List(last.truncate))) case _ => None } } def purge(versions: Map[Document_ID.Version, Version]): History = { val undo_list1 = undo_list.map(_.purge(versions)) if (undo_list1.forall(_.isEmpty)) this else new History(for ((a, b) <- undo_list1 zip undo_list) yield a.getOrElse(b)) } } /* snapshot */ object Snapshot { val init: Snapshot = State.init.snapshot() } abstract class Snapshot { def state: State def version: Version def is_outdated: Boolean def convert(i: Text.Offset): Text.Offset def revert(i: Text.Offset): Text.Offset def convert(range: Text.Range): Text.Range def revert(range: Text.Range): Text.Range 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] def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body def messages: List[(XML.Tree, Position.T)] def exports: List[Export.Entry] def exports_map: Map[String, Export.Entry] def find_command(id: Document_ID.Generic): Option[(Node, Command)] def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset) : Option[Line.Node_Position] def cumulate[A]( range: Text.Range, info: A, elements: Markup.Elements, result: List[Command.State] => (A, Text.Markup) => Option[A], status: Boolean = false): List[Text.Info[A]] def select[A]( range: Text.Range, elements: Markup.Elements, result: List[Command.State] => Text.Markup => Option[A], status: Boolean = false): List[Text.Info[A]] def command_results(range: Text.Range): Command.Results def command_results(command: Command): Command.Results def command_id_map: Map[Document_ID.Generic, Command] } /* model */ trait Session { def resources: Resources } trait Model { def session: Session def is_stable: Boolean def snapshot(): Snapshot def node_name: Node.Name def is_theory: Boolean = node_name.is_theory override def toString: String = node_name.toString def get_text(range: Text.Range): Option[String] def node_required: Boolean def get_blob: Option[Blob] def bibtex_entries: List[Text.Info[String]] def node_edits( node_header: Node.Header, text_edits: List[Text.Edit], perspective: Node.Perspective_Text): List[Edit_Text] = { val edits: List[Node.Edit[Text.Edit, Text.Perspective]] = get_blob match { case None => List( Node.Deps( if (session.resources.session_base.loaded_theory(node_name)) { node_header.append_errors( List("Cannot update finished theory " + quote(node_name.theory))) } else node_header), Node.Edits(text_edits), perspective) case Some(blob) => List(Node.Blob(blob), Node.Edits(text_edits)) } edits.flatMap(edit => if (edit.is_void) None else Some(node_name -> edit)) } } /** global state -- document structure, execution process, editing history **/ type Assign_Update = List[(Document_ID.Command, List[Document_ID.Exec])] // update of exec state assignment object State { class Fail(state: State) extends Exception object Assignment { val init: Assignment = new Assignment() } final class Assignment private( val command_execs: Map[Document_ID.Command, List[Document_ID.Exec]] = Map.empty, val is_finished: Boolean = false) { override def toString: String = "Assignment(" + command_execs.size + "," + is_finished + ")" def check_finished: Assignment = { require(is_finished); this } def unfinished: Assignment = new Assignment(command_execs, false) def assign(update: Assign_Update): Assignment = { require(!is_finished) val command_execs1 = (command_execs /: update) { case (res, (command_id, exec_ids)) => if (exec_ids.isEmpty) res - command_id else res + (command_id -> exec_ids) } new Assignment(command_execs1, true) } } val init: State = State().define_version(Version.init, Assignment.init).assign(Version.init.id, Nil, Nil)._2 } final case class State private( /*reachable versions*/ versions: Map[Document_ID.Version, Version] = Map.empty, /*inlined auxiliary files*/ blobs: Set[SHA1.Digest] = Set.empty, /*static markup from define_command*/ commands: Map[Document_ID.Command, Command.State] = Map.empty, /*dynamic markup from execution*/ execs: Map[Document_ID.Exec, Command.State] = Map.empty, /*command-exec assignment for each version*/ assignments: Map[Document_ID.Version, State.Assignment] = Map.empty, /*commands with markup produced by other commands (imm_succs)*/ commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long, /*explicit (linear) history*/ history: History = History.init, /*intermediate state between remove_versions/removed_versions*/ removing_versions: Boolean = false) { override def toString: String = "State(versions = " + versions.size + ", blobs = " + blobs.size + ", commands = " + commands.size + ", execs = " + execs.size + ", assignments = " + assignments.size + ", commands_redirection = " + commands_redirection.size + ", history = " + history.undo_list.size + ", removing_versions = " + removing_versions + ")" private def fail[A]: A = throw new State.Fail(this) def define_version(version: Version, assignment: State.Assignment): State = { val id = version.id copy(versions = versions + (id -> version), assignments = assignments + (id -> assignment.unfinished)) } def define_blob(digest: SHA1.Digest): State = copy(blobs = blobs + digest) def defined_blob(digest: SHA1.Digest): Boolean = blobs.contains(digest) def define_command(command: Command): State = { val id = command.id copy(commands = commands + (id -> command.init_state)) } def defined_command(id: Document_ID.Command): Boolean = commands.isDefinedAt(id) def the_version(id: Document_ID.Version): Version = versions.getOrElse(id, fail) def the_static_state(id: Document_ID.Command): Command.State = commands.getOrElse(id, fail) def the_dynamic_state(id: Document_ID.Exec): Command.State = execs.getOrElse(id, fail) def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version.id, fail) def lookup_id(id: Document_ID.Generic): Option[Command.State] = commands.get(id) orElse execs.get(id) private def self_id(st: Command.State)(id: Document_ID.Generic): Boolean = id == st.command.id || (execs.get(id) match { case Some(st1) => st1.command.id == st.command.id case None => false }) private def other_id(id: Document_ID.Generic) : Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)] = lookup_id(id).map(st => ((Symbol.Text_Chunk.Id(st.command.id), st.command.chunk))) private def redirection(st: Command.State): Graph[Document_ID.Command, Unit] = (commands_redirection /: st.markups.redirection_iterator)({ case (graph, id) => graph.default_node(id, ()).default_node(st.command.id, ()).add_edge(id, st.command.id) }) def accumulate(id: Document_ID.Generic, message: XML.Elem, xml_cache: XML.Cache) : (Command.State, State) = { execs.get(id) match { case Some(st) => val new_st = st.accumulate(self_id(st), other_id, message, xml_cache) val execs1 = execs + (id -> new_st) (new_st, copy(execs = execs1, commands_redirection = redirection(new_st))) case None => commands.get(id) match { case Some(st) => val new_st = st.accumulate(self_id(st), other_id, message, xml_cache) val commands1 = commands + (id -> new_st) (new_st, copy(commands = commands1, commands_redirection = redirection(new_st))) case None => fail } } } def add_export(id: Document_ID.Generic, entry: Command.Exports.Entry): (Command.State, State) = { execs.get(id) match { case Some(st) => st.add_export(entry) match { case Some(new_st) => (new_st, copy(execs = execs + (id -> new_st))) case None => fail } case None => commands.get(id) match { case Some(st) => st.add_export(entry) match { case Some(new_st) => (new_st, copy(commands = commands + (id -> new_st))) case None => fail } case None => fail } } } def node_exports(version: Version, node_name: Node.Name): Command.Exports = Command.Exports.merge( for { command <- version.nodes(node_name).commands.iterator st <- command_states(version, command).iterator } yield st.exports) def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update) : ((List[Node.Name], List[Command]), State) = { val version = the_version(id) val edited_set = edited.toSet val edited_nodes = (for { (name, _) <- version.nodes.iterator if edited_set(name.node) } yield name).toList def upd(exec_id: Document_ID.Exec, st: Command.State) : Option[(Document_ID.Exec, Command.State)] = if (execs.isDefinedAt(exec_id)) None else Some(exec_id -> st) val (changed_commands, new_execs) = ((Nil: List[Command], execs) /: update) { case ((commands1, execs1), (command_id, exec)) => val st = the_static_state(command_id) val command = st.command val commands2 = command :: commands1 val execs2 = exec match { case Nil => execs1 case eval_id :: print_ids => execs1 ++ upd(eval_id, st) ++ (for (id <- print_ids; up <- upd(id, command.empty_state)) yield up) } (commands2, execs2) } val new_assignment = the_assignment(version).assign(update) val new_state = copy(assignments = assignments + (id -> new_assignment), execs = new_execs) ((edited_nodes, changed_commands), new_state) } def is_assigned(version: Version): Boolean = assignments.get(version.id) match { case Some(assgn) => assgn.is_finished case None => false } def is_stable(change: Change): Boolean = change.is_finished && is_assigned(change.version.get_finished) def recent_finished: Change = history.undo_list.find(_.is_finished) getOrElse fail def recent_stable: Change = history.undo_list.find(is_stable) getOrElse fail def stable_tip_version: Option[Version] = if (is_stable(history.tip)) Some(history.tip.version.get_finished) else None def continue_history( previous: Future[Version], edits: List[Edit_Text], version: Future[Version]): State = { val change = Change.make(previous, edits, version) copy(history = history + change) } def remove_versions(retain: Int = 0): (List[Version], State) = { history.prune(is_stable, retain) match { case Some((dropped, history1)) => val old_versions = dropped.map(change => change.version.get_finished) val removing = old_versions.nonEmpty val state1 = copy(history = history1, removing_versions = removing) (old_versions, state1) case None => fail } } def removed_versions(removed: List[Document_ID.Version]): State = { val versions1 = Version.purge_suppressed(versions -- removed) val assignments1 = assignments -- removed var blobs1_names = Set.empty[Node.Name] var blobs1 = Set.empty[SHA1.Digest] var commands1 = Map.empty[Document_ID.Command, Command.State] var execs1 = Map.empty[Document_ID.Exec, Command.State] for { (version_id, version) <- versions1.iterator command_execs = assignments1(version_id).command_execs (_, node) <- version.nodes.iterator command <- node.commands.iterator } { for ((name, digest) <- command.blobs_defined) { blobs1_names += name blobs1 += digest } if (!commands1.isDefinedAt(command.id)) commands.get(command.id).foreach(st => commands1 += (command.id -> st)) for (exec_id <- command_execs.getOrElse(command.id, Nil)) { if (!execs1.isDefinedAt(exec_id)) execs.get(exec_id).foreach(st => execs1 += (exec_id -> st)) } } copy( versions = versions1, blobs = blobs1, commands = commands1, execs = execs1, commands_redirection = commands_redirection.restrict(commands1.keySet), assignments = assignments1, history = history.purge(versions1), removing_versions = false) } def command_id_map(version: Version, commands: Iterable[Command]) : Map[Document_ID.Generic, Command] = { require(is_assigned(version)) val assignment = the_assignment(version).check_finished (for { command <- commands.iterator id <- (command.id :: assignment.command_execs.getOrElse(command.id, Nil)).iterator } yield (id -> command)).toMap } def command_maybe_consolidated(version: Version, command: Command): Boolean = { require(is_assigned(version)) try { the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) match { case eval_id :: print_ids => the_dynamic_state(eval_id).maybe_consolidated && !print_ids.exists(print_id => the_dynamic_state(print_id).consolidating) case Nil => false } } catch { case _: State.Fail => false } } private def command_states_self(version: Version, command: Command) : List[(Document_ID.Generic, Command.State)] = { require(is_assigned(version)) try { the_assignment(version).check_finished.command_execs.getOrElse(command.id, Nil) .map(id => id -> the_dynamic_state(id)) match { case Nil => fail case res => res } } catch { case _: State.Fail => try { List(command.id -> the_static_state(command.id)) } catch { case _: State.Fail => List(command.id -> command.init_state) } } } def command_states(version: Version, command: Command): List[Command.State] = { val self = command_states_self(version, command) val others = if (commands_redirection.defined(command.id)) { (for { command_id <- commands_redirection.imm_succs(command.id).iterator (id, st) <- command_states_self(version, the_static_state(command_id).command) if !self.exists(_._1 == id) } yield (id, st)).toMap.valuesIterator.toList } else Nil self.map(_._2) ::: others.flatMap(_.redirect(command)) } def command_results(version: Version, command: Command): Command.Results = Command.State.merge_results(command_states(version, command)) def command_markup(version: Version, command: Command, index: Command.Markup_Index, range: Text.Range, elements: Markup.Elements): Markup_Tree = Command.State.merge_markup(command_states(version, command), index, range, elements) def markup_to_XML( version: Version, node_name: Node.Name, range: Text.Range, elements: Markup.Elements): XML.Body = { val node = version.nodes(node_name) if (node_name.is_theory) { val markup_index = Command.Markup_Index.markup (for { command <- node.commands.iterator command_range <- command.range.try_restrict(range).iterator markup = command_markup(version, command, markup_index, command_range, elements) tree <- markup.to_XML(command_range, command.source, elements).iterator } yield tree).toList } else { val node_source = node.source Text.Range(0, node_source.length).try_restrict(range) match { case None => Nil case Some(node_range) => val markup = version.nodes.commands_loading(node_name).headOption match { case None => Markup_Tree.empty case Some(command) => val chunk_name = Symbol.Text_Chunk.File(node_name.node) val markup_index = Command.Markup_Index(false, chunk_name) command_markup(version, command, markup_index, node_range, elements) } markup.to_XML(node_range, node_source, elements) } } } 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_maybe_consolidated(version: Version, name: Node.Name): Boolean = name.is_theory && version.nodes(name).commands.reverse.iterator.forall(command_maybe_consolidated(version, _)) def node_consolidated(version: Version, name: Node.Name): Boolean = !name.is_theory || { val it = version.nodes(name).commands.reverse.iterator it.hasNext && command_states(version, it.next).exists(_.consolidated) } // persistent user-view def snapshot(name: Node.Name = Node.Name.empty, pending_edits: List[Text.Edit] = Nil) : Snapshot = { val stable = recent_stable val latest = history.tip /* pending edits and unstable changes */ val rev_pending_changes = for { change <- history.undo_list.takeWhile(_ != stable) (a, edits) <- change.rev_edits if a == name } yield edits val edits = (pending_edits /: rev_pending_changes)({ case (edits, Node.Edits(es)) => es ::: edits case (edits, _) => edits }) lazy val reverse_edits = edits.reverse new Snapshot { /* global information */ val state: State = State.this val version: Version = stable.version.get_finished val is_outdated: Boolean = pending_edits.nonEmpty || latest != stable /* local node content */ def convert(offset: Text.Offset): Text.Offset = (offset /: edits)((i, edit) => edit.convert(i)) def revert(offset: Text.Offset): Text.Offset = (offset /: reverse_edits)((i, edit) => edit.revert(i)) def convert(range: Text.Range): Text.Range = range.map(convert) def revert(range: Text.Range): Text.Range = range.map(revert) 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) def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range] = (for { cmd <- node.load_commands.iterator blob_name <- cmd.blobs_names.iterator if pred(blob_name) start <- node.command_start(cmd) } yield convert(cmd.core_range + start)).toList def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] = if (other_node_name.is_theory) { val other_node = version.nodes(other_node_name) val iterator = other_node.command_iterator(revert(offset) max 0) if (iterator.hasNext) { val (command0, _) = iterator.next other_node.commands.reverse.iterator(command0).find(command => !command.is_ignored) } else other_node.commands.reverse.iterator.find(command => !command.is_ignored) } else version.nodes.commands_loading(other_node_name).headOption def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body = state.markup_to_XML(version, node_name, range, elements) lazy val messages: List[(XML.Tree, Position.T)] = (for { (command, start) <- Document.Node.Commands.starts_pos( node.commands.iterator, Token.Pos.file(node_name.node)) pos = command.span.keyword_pos(start).position(command.span.name) (_, tree) <- state.command_results(version, command).iterator } yield (tree, pos)).toList lazy val exports: List[Export.Entry] = state.node_exports(version, node_name).iterator.map(_._2).toList lazy val exports_map: Map[String, Export.Entry] = (for (entry <- exports.iterator) yield (entry.name, entry)).toMap /* find command */ def find_command(id: Document_ID.Generic): Option[(Node, Command)] = state.lookup_id(id) match { case None => None case Some(st) => val command = st.command val node = version.nodes(command.node_name) if (node.commands.contains(command)) Some((node, command)) else None } def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset) : Option[Line.Node_Position] = for ((node, command) <- find_command(id)) yield { val name = command.node_name.node val sources_iterator = node.commands.iterator.takeWhile(_ != command).map(_.source) ++ (if (offset == 0) Iterator.empty else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset))))) val pos = (Line.Position.zero /: sources_iterator)(_.advance(_)) Line.Node_Position(name, pos) } /* cumulate markup */ def cumulate[A]( range: Text.Range, info: A, elements: Markup.Elements, result: List[Command.State] => (A, Text.Markup) => Option[A], status: Boolean = false): List[Text.Info[A]] = { val former_range = revert(range).inflate_singularity val (chunk_name, command_iterator) = commands_loading.headOption match { case None => (Symbol.Text_Chunk.Default, node.command_iterator(former_range)) case Some(command) => (Symbol.Text_Chunk.File(node_name.node), Iterator((command, 0))) } val markup_index = Command.Markup_Index(status, chunk_name) (for { (command, command_start) <- command_iterator chunk <- command.chunks.get(chunk_name).iterator states = state.command_states(version, command) res = result(states) markup_range <- (former_range - command_start).try_restrict(chunk.range).iterator markup = Command.State.merge_markup(states, markup_index, markup_range, elements) Text.Info(r0, a) <- markup.cumulate[A](markup_range, info, elements, { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b)) }).iterator r1 <- convert(r0 + command_start).try_restrict(range).iterator } yield Text.Info(r1, a)).toList } def select[A]( range: Text.Range, elements: Markup.Elements, result: List[Command.State] => Text.Markup => Option[A], status: Boolean = false): List[Text.Info[A]] = { def result1(states: List[Command.State]): (Option[A], Text.Markup) => Option[Option[A]] = { val res = result(states) (_: Option[A], x: Text.Markup) => res(x) match { case None => None case some => Some(some) } } for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1, status)) yield Text.Info(r, x) } /* command results */ def command_results(range: Text.Range): Command.Results = Command.State.merge_results( select[List[Command.State]](range, Markup.Elements.full, command_states => { case _ => Some(command_states) }).flatMap(_.info)) def command_results(command: Command): Command.Results = state.command_results(version, command) /* command ids: static and dynamic */ def command_id_map: Map[Document_ID.Generic, Command] = state.command_id_map(version, version.nodes(node_name).commands) /* output */ override def toString: String = "Snapshot(node = " + node_name.node + ", version = " + version.id + (if (is_outdated) ", outdated" else "") + ")" } } } } diff --git a/src/Pure/PIDE/headless.scala b/src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala +++ b/src/Pure/PIDE/headless.scala @@ -1,661 +1,661 @@ /* Title: Pure/PIDE/headless.scala Author: Makarius Headless PIDE session and resources from file-system. */ package isabelle import java.io.{File => JFile} import scala.annotation.tailrec import scala.collection.mutable object Headless { /** session **/ private def stable_snapshot( state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot = { val snapshot = state.snapshot(name) assert(version.id == snapshot.version.id) snapshot } class Use_Theories_Result private[Headless]( val state: Document.State, val version: Document.Version, val nodes: List[(Document.Node.Name, Document_Status.Node_Status)], val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)]) { def nodes_pending: List[(Document.Node.Name, Document_Status.Node_Status)] = { val committed = nodes_committed.iterator.map(_._1).toSet nodes.filter(p => !committed(p._1)) } def snapshot(name: Document.Node.Name): Document.Snapshot = stable_snapshot(state, version, name) def ok: Boolean = (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok }) } class Session private[Headless]( session_name: String, _session_options: => Options, override val resources: Resources) extends isabelle.Session(_session_options, resources) { session => private def loaded_theory(name: Document.Node.Name): Boolean = resources.session_base.loaded_theory(name.theory) /* options */ override def consolidate_delay: Time = session_options.seconds("headless_consolidate_delay") override def prune_delay: Time = session_options.seconds("headless_prune_delay") def default_check_delay: Time = session_options.seconds("headless_check_delay") def default_check_limit: Int = session_options.int("headless_check_limit") def default_nodes_status_delay: Time = session_options.seconds("headless_nodes_status_delay") def default_watchdog_timeout: Time = session_options.seconds("headless_watchdog_timeout") def default_commit_cleanup_delay: Time = session_options.seconds("headless_commit_cleanup_delay") /* temporary directory */ val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session") val tmp_dir_name: String = File.path(tmp_dir).implode def master_directory(master_dir: String): String = proper_string(master_dir) getOrElse tmp_dir_name override def toString: String = session_name override def stop(): Process_Result = { try { super.stop() } finally { Isabelle_System.rm_tree(tmp_dir) } } /* theories */ private object Load_State { def finished: Load_State = Load_State(Nil, Nil, 0) def count_file(name: Document.Node.Name): Long = if (loaded_theory(name)) 0 else name.path.file.length } private case class Load_State( pending: List[Document.Node.Name], rest: List[Document.Node.Name], load_limit: Long) { def next( dep_graph: Document.Node.Name.Graph[Unit], finished: Document.Node.Name => Boolean): (List[Document.Node.Name], Load_State) = { def load_requirements(pending1: List[Document.Node.Name], rest1: List[Document.Node.Name]) : (List[Document.Node.Name], Load_State) = { - val load_theories = dep_graph.all_preds(pending1).reverse.filterNot(finished) + val load_theories = dep_graph.all_preds_rev(pending1).filterNot(finished) (load_theories, Load_State(pending1, rest1, load_limit)) } if (!pending.forall(finished)) (Nil, this) else if (rest.isEmpty) (Nil, Load_State.finished) else if (load_limit == 0) load_requirements(rest, Nil) else { val reachable = dep_graph.reachable_limit(load_limit, Load_State.count_file, dep_graph.imm_preds, rest) val (pending1, rest1) = rest.partition(reachable) load_requirements(pending1, rest1) } } } private sealed case class Use_Theories_State( dep_graph: Document.Node.Name.Graph[Unit], load_state: Load_State, watchdog_timeout: Time, commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit], last_update: Time = Time.now(), nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty, already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty, result: Option[Exn.Result[Use_Theories_Result]] = None) { def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State = copy(last_update = Time.now(), nodes_status = new_nodes_status) def watchdog: Boolean = watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout def finished_result: Boolean = result.isDefined def join_result: Option[(Exn.Result[Use_Theories_Result], Use_Theories_State)] = if (finished_result) Some((result.get, this)) else None def cancel_result: Use_Theories_State = if (finished_result) this else copy(result = Some(Exn.Exn(Exn.Interrupt()))) def clean_theories: (List[Document.Node.Name], Use_Theories_State) = { @tailrec def frontier(base: List[Document.Node.Name], front: Set[Document.Node.Name]) : Set[Document.Node.Name] = { val add = base.filter(name => dep_graph.imm_succs(name).forall(front)) if (add.isEmpty) front else { val preds = add.map(dep_graph.imm_preds) val base1 = (preds.head /: preds.tail)(_ ++ _).toList.filter(already_committed.keySet) frontier(base1, front ++ add) } } if (already_committed.isEmpty) (Nil, this) else { val base = (for { (name, (_, (_, succs))) <- dep_graph.iterator if succs.isEmpty && already_committed.isDefinedAt(name) } yield name).toList val clean = frontier(base, Set.empty) if (clean.isEmpty) (Nil, this) else { (dep_graph.topological_order.filter(clean), copy(dep_graph = dep_graph.exclude(clean))) } } } def check(state: Document.State, version: Document.Version, beyond_limit: Boolean) : (List[Document.Node.Name], Use_Theories_State) = { val already_committed1 = commit match { case None => already_committed case Some(commit_fn) => (already_committed /: dep_graph.topological_order)( { case (committed, name) => def parents_committed: Boolean = version.nodes(name).header.imports.forall(parent => loaded_theory(parent) || committed.isDefinedAt(parent)) if (!committed.isDefinedAt(name) && parents_committed && state.node_consolidated(version, name)) { val snapshot = stable_snapshot(state, version, name) val status = Document_Status.Node_Status.make(state, version, name) commit_fn(snapshot, status) committed + (name -> status) } else committed }) } def finished_theory(name: Document.Node.Name): Boolean = loaded_theory(name) || (if (commit.isDefined) already_committed1.isDefinedAt(name) else state.node_consolidated(version, name)) val result1 = if (!finished_result && (beyond_limit || watchdog || dep_graph.keys_iterator.forall(name => finished_theory(name) || nodes_status.quasi_consolidated(name)))) { val nodes = (for { name <- dep_graph.keys_iterator if !loaded_theory(name) } yield { (name -> Document_Status.Node_Status.make(state, version, name)) }).toList val nodes_committed = (for { name <- dep_graph.keys_iterator status <- already_committed1.get(name) } yield (name -> status)).toList Some(Exn.Res(new Use_Theories_Result(state, version, nodes, nodes_committed))) } else result val (load_theories, load_state1) = load_state.next(dep_graph, finished_theory) (load_theories, copy(already_committed = already_committed1, result = result1, load_state = load_state1)) } } def use_theories( theories: List[String], qualifier: String = Sessions.DRAFT, master_dir: String = "", unicode_symbols: Boolean = false, check_delay: Time = default_check_delay, check_limit: Int = default_check_limit, watchdog_timeout: Time = default_watchdog_timeout, nodes_status_delay: Time = default_nodes_status_delay, id: UUID.T = UUID.random(), // commit: must not block, must not fail commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None, commit_cleanup_delay: Time = default_commit_cleanup_delay, progress: Progress = new Progress): Use_Theories_Result = { 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 } val dep_theories = dependencies.theories val dep_theories_set = dep_theories.toSet val dep_files = dependencies.loaded_files(false).flatMap(_._2). map(path => Document.Node.Name(resources.append("", path))) val use_theories_state = { val dep_graph = dependencies.theory_graph val maximals = dep_graph.maximals val rest = if (maximals.isEmpty || maximals.tail.isEmpty) maximals else { val depth = dep_graph.node_depth(Load_State.count_file) maximals.sortBy(node => - depth(node)) } val load_limit = if (commit.isDefined) (session_options.real("headless_load_limit") * 1024 * 1024).round else 0 val load_state = Load_State(Nil, rest, load_limit) Synchronized(Use_Theories_State(dep_graph, load_state, watchdog_timeout, commit)) } def check_state(beyond_limit: Boolean = false) { val state = session.get_state() for { version <- state.stable_tip_version load_theories = use_theories_state.change_result(_.check(state, version, beyond_limit)) if load_theories.nonEmpty } resources.load_theories(session, id, load_theories, dep_files, unicode_symbols, progress) } val check_progress = { var check_count = 0 Event_Timer.request(Time.now(), repeat = Some(check_delay)) { if (progress.stopped) use_theories_state.change(_.cancel_result) else { check_count += 1 check_state(check_limit > 0 && check_count > check_limit) } } } val consumer = { val delay_nodes_status = Delay.first(nodes_status_delay max Time.zero) { progress.nodes_status(use_theories_state.value.nodes_status) } val delay_commit_clean = Delay.first(commit_cleanup_delay max Time.zero) { val clean_theories = use_theories_state.change_result(_.clean_theories) if (clean_theories.nonEmpty) { progress.echo("Removing " + clean_theories.length + " theories ...") resources.clean_theories(session, id, clean_theories) } } Session.Consumer[Session.Commands_Changed](getClass.getName) { case changed => if (changed.nodes.exists(dep_theories_set)) { val snapshot = session.snapshot() val state = snapshot.state val version = snapshot.version val theory_progress = use_theories_state.change_result(st => { val domain = if (st.nodes_status.is_empty) dep_theories_set else changed.nodes.iterator.filter(dep_theories_set).toSet val (nodes_status_changed, nodes_status1) = st.nodes_status.update(resources, state, version, domain = Some(domain), trim = changed.assignment) if (nodes_status_delay >= Time.zero && nodes_status_changed) { delay_nodes_status.invoke } val theory_progress = (for { (name, node_status) <- nodes_status1.present.iterator if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name) p1 = node_status.percentage if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage) } yield Progress.Theory(name.theory, percentage = Some(p1))).toList (theory_progress, st.update(nodes_status1)) }) theory_progress.foreach(progress.theory) check_state() if (commit.isDefined && commit_cleanup_delay > Time.zero) { if (use_theories_state.value.finished_result) delay_commit_clean.revoke else delay_commit_clean.invoke } } } } try { session.commands_changed += consumer check_state() use_theories_state.guarded_access(_.join_result) check_progress.cancel } finally { session.commands_changed -= consumer resources.unload_theories(session, id, dep_theories) } Exn.release(use_theories_state.guarded_access(_.join_result)) } def purge_theories( theories: List[String], qualifier: String = Sessions.DRAFT, master_dir: String = "", all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) = { val nodes = if (all) None else Some(theories.map(resources.import_name(qualifier, master_directory(master_dir), _))) resources.purge_theories(session, nodes) } } /** resources **/ object Resources { def apply(options: Options, base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources = new Resources(options, base_info, log = log) def make( options: Options, session_name: String, session_dirs: List[Path] = Nil, include_sessions: List[String] = Nil, progress: Progress = new Progress, log: Logger = No_Logger): Resources = { val base_info = Sessions.base_info(options, session_name, dirs = session_dirs, include_sessions = include_sessions, progress = progress) apply(options, base_info, log = log) } final class Theory private[Headless]( val node_name: Document.Node.Name, val node_header: Document.Node.Header, val text: String, val node_required: Boolean) { override def toString: String = node_name.toString def node_perspective: Document.Node.Perspective_Text = Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty) def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] = List(node_name -> Document.Node.Deps(node_header), node_name -> Document.Node.Edits(text_edits), node_name -> node_perspective) def node_edits(old: Option[Theory]): List[Document.Edit_Text] = { val (text_edits, old_required) = if (old.isEmpty) (Text.Edit.inserts(0, text), false) else (Text.Edit.replace(0, old.get.text, text), old.get.node_required) if (text_edits.isEmpty && node_required == old_required) Nil else make_edits(text_edits) } def purge_edits: List[Document.Edit_Text] = make_edits(Text.Edit.removes(0, text)) def required(required: Boolean): Theory = if (required == node_required) this else new Theory(node_name, node_header, text, required) } sealed case class State( 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: Document.Node.Name.Graph[Unit] = Document.Node.Name.make_graph( for ((name, theory) <- theories.toList) yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt))) def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name) def insert_required(id: UUID.T, names: List[Document.Node.Name]): State = copy(required = (required /: names)(_.insert(_, id))) def remove_required(id: UUID.T, names: List[Document.Node.Name]): State = copy(required = (required /: names)(_.remove(_, id))) def update_theories(update: List[(Document.Node.Name, Theory)]): State = copy(theories = (theories /: update)({ case (thys, (name, thy)) => thys.get(name) match { case Some(thy1) if thy1 == thy => thys case _ => thys + (name -> thy) } })) def remove_theories(remove: List[Document.Node.Name]): State = { require(remove.forall(name => !is_required(name))) copy(theories = theories -- remove) } def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) : (List[Document.Edit_Text], State) = { val st1 = remove_required(id, theories) val theory_edits = for { node_name <- theories theory <- st1.theories.get(node_name) } yield { val theory1 = theory.required(st1.is_required(node_name)) val edits = theory1.node_edits(Some(theory)) (edits, (node_name, theory1)) } (theory_edits.flatMap(_._1), st1.update_theories(theory_edits.map(_._2))) } def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]]) : ((List[Document.Node.Name], List[Document.Node.Name], List[Document.Edit_Text]), State) = { val all_nodes = theory_graph.topological_order val purge = nodes.getOrElse(all_nodes).filterNot(is_required).toSet val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet val (retained, purged) = all_nodes.partition(retain) val purge_edits = purged.flatMap(name => theories(name).purge_edits) ((purged, retained, purge_edits), remove_theories(purged)) } } } class Resources private[Headless]( val options: Options, val session_base_info: Sessions.Base_Info, log: Logger = No_Logger) extends isabelle.Resources( session_base_info.sessions_structure, session_base_info.check_base, log = log) { resources => val store: Sessions.Store = Sessions.store(options) /* session */ def start_session(print_mode: List[String] = Nil, progress: Progress = new Progress): Session = { val session = new Session(session_base_info.session, options, resources) progress.echo("Starting session " + session_base_info.session + " ...") Isabelle_Process(session, options, session_base_info.sessions_structure, store, logic = session_base_info.session, modes = print_mode).await_startup session } /* theories */ private val state = Synchronized(Resources.State()) def load_theories( session: Session, id: UUID.T, theories: List[Document.Node.Name], files: List[Document.Node.Name], unicode_symbols: Boolean, progress: Progress) { val loaded_theories = for (node_name <- theories) yield { val path = node_name.path if (!node_name.is_theory) error("Not a theory file: " + path) progress.expose_interrupt() val text0 = File.read(path) val text = if (unicode_symbols) Symbol.decode(text0) else text0 val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text)) new Resources.Theory(node_name, node_header, text, true) } val loaded = loaded_theories.length if (loaded > 1) progress.echo("Loading " + loaded + " theories ...") state.change(st => { val (doc_blobs1, st1) = st.insert_required(id, theories).update_blobs(files) val theory_edits = for (theory <- loaded_theories) yield { val node_name = theory.node_name val theory1 = theory.required(st1.is_required(node_name)) val edits = theory1.node_edits(st1.theories.get(node_name)) (edits, (node_name, theory1)) } val file_edits = for { node_name <- 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)) }) } def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) { state.change(st => { val (edits, st1) = st.unload_theories(session, id, theories) session.update(st.doc_blobs, edits) st1 }) } def clean_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) { state.change(st => { val (edits1, st1) = st.unload_theories(session, id, theories) val ((_, _, edits2), st2) = st1.purge_theories(session, None) session.update(st.doc_blobs, edits1 ::: edits2) st2 }) } def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]]) : (List[Document.Node.Name], List[Document.Node.Name]) = { state.change_result(st => { val ((purged, retained, _), st1) = st.purge_theories(session, nodes) ((purged, retained), st1) }) } } } diff --git a/src/Pure/Thy/sessions.scala b/src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala +++ b/src/Pure/Thy/sessions.scala @@ -1,1297 +1,1297 @@ /* Title: Pure/Thy/sessions.scala Author: Makarius Cumulative session information. */ package isabelle import java.io.{File => JFile} import java.nio.ByteBuffer import java.nio.channels.FileChannel import java.nio.file.StandardOpenOption import scala.collection.{SortedSet, SortedMap} import scala.collection.mutable object Sessions { /* session and theory names */ val root_name: String = "ROOT" val theory_name: String = "Pure.Sessions" val UNSORTED = "Unsorted" val DRAFT = "Draft" def is_pure(name: String): Boolean = name == Thy_Header.PURE def exclude_session(name: String): Boolean = name == "" || name == DRAFT def exclude_theory(name: String): Boolean = name == root_name || name == "README" || name == "index" || name == "bib" /* base info and source dependencies */ object Base { def bootstrap( session_directories: Map[JFile, String], global_theories: Map[String, String]): Base = Base( session_directories = session_directories, global_theories = global_theories, overall_syntax = Thy_Header.bootstrap_syntax) } sealed case class Base( pos: Position.T = Position.none, doc_names: List[String] = Nil, session_directories: Map[JFile, String] = Map.empty, global_theories: Map[String, String] = Map.empty, loaded_theories: Graph[String, Outer_Syntax] = Graph.string, used_theories: List[(Document.Node.Name, Options)] = Nil, known_theories: Map[String, Document.Node.Entry] = Map.empty, known_loaded_files: Map[String, List[Path]] = Map.empty, overall_syntax: Outer_Syntax = Outer_Syntax.empty, imported_sources: List[(Path, SHA1.Digest)] = Nil, sources: List[(Path, SHA1.Digest)] = Nil, session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph, errors: List[String] = Nil) { override def toString: String = "Sessions.Base(loaded_theories = " + loaded_theories.size + ", used_theories = " + used_theories.length + ")" def theory_qualifier(name: String): String = global_theories.getOrElse(name, Long_Name.qualifier(name)) def theory_qualifier(name: Document.Node.Name): String = theory_qualifier(name.theory) def loaded_theory(name: String): Boolean = loaded_theories.defined(name) def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory) def loaded_theory_syntax(name: String): Option[Outer_Syntax] = if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] = loaded_theory_syntax(name.theory) def node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Outer_Syntax = nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax } sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) { override def toString: String = "Sessions.Deps(" + sessions_structure + ")" def is_empty: Boolean = session_bases.isEmpty def apply(name: String): Base = session_bases(name) def get(name: String): Option[Base] = session_bases.get(name) def imported_sources(name: String): List[SHA1.Digest] = session_bases(name).imported_sources.map(_._2) def sources(name: String): List[SHA1.Digest] = session_bases(name).sources.map(_._2) def errors: List[String] = (for { (name, base) <- session_bases.iterator if base.errors.nonEmpty } yield cat_lines(base.errors) + "\nThe error(s) above occurred in session " + quote(name) + Position.here(base.pos) ).toList def check_errors: Deps = errors match { case Nil => this case errs => error(cat_lines(errs)) } } def deps(sessions_structure: Structure, progress: Progress = new Progress, inlined_files: Boolean = false, verbose: Boolean = false, list_files: Boolean = false, check_keywords: Set[String] = Set.empty): Deps = { var cache_sources = Map.empty[JFile, SHA1.Digest] def check_sources(paths: List[Path]): List[(Path, SHA1.Digest)] = { for { path <- paths file = path.file if cache_sources.isDefinedAt(file) || file.isFile } yield { cache_sources.get(file) match { case Some(digest) => (path, digest) case None => val digest = SHA1.digest(file) cache_sources = cache_sources + (file -> digest) (path, digest) } } } val doc_names = Doc.doc_names() val bootstrap = Sessions.Base.bootstrap( sessions_structure.session_directories, sessions_structure.global_theories) val session_bases = (Map("" -> bootstrap) /: sessions_structure.imports_topological_order)({ case (session_bases, session_name) => progress.expose_interrupt() val info = sessions_structure(session_name) try { val parent_base = session_bases(info.parent.getOrElse("")) val imports_base: Sessions.Base = { val imports_bases = info.imports.map(session_bases(_)) parent_base.copy( known_theories = (parent_base.known_theories /: (for { base <- imports_bases.iterator (_, entry) <- base.known_theories.iterator } yield (entry.name.theory -> entry)))(_ + _), known_loaded_files = (parent_base.known_loaded_files /: imports_bases.iterator.map(_.known_loaded_files))(_ ++ _)) } val resources = new Resources(sessions_structure, imports_base) if (verbose || list_files) { val groups = if (info.groups.isEmpty) "" else info.groups.mkString(" (", " ", ")") progress.echo("Session " + info.chapter + "/" + info.name + groups) } val dependencies = resources.session_dependencies(info) val overall_syntax = dependencies.overall_syntax val theory_files = dependencies.theories.map(_.path) val loaded_files = if (inlined_files) dependencies.loaded_files(Sessions.is_pure(info.name)) else Nil val session_files = (theory_files ::: loaded_files.flatMap(_._2) ::: info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand) val imported_files = if (inlined_files) dependencies.imported_files else Nil if (list_files) progress.echo(cat_lines(session_files.map(_.implode).sorted.map(" " + _))) if (check_keywords.nonEmpty) { Check_Keywords.check_keywords( progress, overall_syntax.keywords, check_keywords, theory_files) } val session_graph_display: Graph_Display.Graph = { def session_node(name: String): Graph_Display.Node = Graph_Display.Node("[" + name + "]", "session." + name) def node(name: Document.Node.Name): Graph_Display.Node = { val qualifier = imports_base.theory_qualifier(name) if (qualifier == info.name) Graph_Display.Node(name.theory_base_name, "theory." + name.theory) else session_node(qualifier) } val required_sessions = dependencies.loaded_theories.all_preds(dependencies.theories.map(_.theory)) .map(theory => imports_base.theory_qualifier(theory)) .filter(name => name != info.name && sessions_structure.defined(name)) val required_subgraph = sessions_structure.imports_graph .restrict(sessions_structure.imports_graph.all_preds(required_sessions).toSet) .transitive_closure .restrict(required_sessions.toSet) .transitive_reduction_acyclic val graph0 = (Graph_Display.empty_graph /: required_subgraph.topological_order)( { case (g, session) => val a = session_node(session) val bs = required_subgraph.imm_preds(session).toList.map(session_node) ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) }) (graph0 /: dependencies.entries)( { case (g, entry) => val a = node(entry.name) val bs = entry.header.imports.map(node).filterNot(_ == a) ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) }) } val known_theories = (imports_base.known_theories /: dependencies.entries.iterator.map(entry => entry.name.theory -> entry))(_ + _) val known_loaded_files = imports_base.known_loaded_files ++ loaded_files val used_theories_session = dependencies.theories.filter(name => imports_base.theory_qualifier(name) == session_name) val dir_errors = { val ok = info.dirs.map(_.canonical_file).toSet val bad = (for { name <- used_theories_session.iterator path = name.master_dir_path if !ok(path.canonical_file) path1 = File.relative_path(info.dir.canonical, path).getOrElse(path) } yield (path1, name)).toList val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).distinct.sorted val errs1 = for { (path1, name) <- bad } yield "Implicit use of directory " + path1 + " for theory " + quote(name.toString) val errs2 = if (bad_dirs.isEmpty) Nil else List("Implicit use of session directories: " + commas(bad_dirs)) val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p val errs4 = (for { name <- used_theories_session.iterator name1 <- resources.find_theory_node(name.theory) if name.node != name1.node } yield "Incoherent theory file import:\n " + name.path + " vs. \n " + name1.path) .toList errs1 ::: errs2 ::: errs3 ::: errs4 } val sources_errors = for (p <- session_files if !p.is_file) yield "No such file: " + p val path_errors = try { Path.check_case_insensitive(session_files ::: imported_files); Nil } catch { case ERROR(msg) => List(msg) } val bibtex_errors = try { info.bibtex_entries; Nil } catch { case ERROR(msg) => List(msg) } val base = Base( pos = info.pos, doc_names = doc_names, session_directories = sessions_structure.session_directories, global_theories = sessions_structure.global_theories, loaded_theories = dependencies.loaded_theories, used_theories = dependencies.theories_adjunct, known_theories = known_theories, known_loaded_files = known_loaded_files, overall_syntax = overall_syntax, imported_sources = check_sources(imported_files), sources = check_sources(session_files), session_graph_display = session_graph_display, errors = dependencies.errors ::: dir_errors ::: sources_errors ::: path_errors ::: bibtex_errors) session_bases + (info.name -> base) } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in session " + quote(info.name) + Position.here(info.pos)) } }) Deps(sessions_structure, session_bases) } /* base info */ sealed case class Base_Info( session: String, sessions_structure: Structure, errors: List[String], base: Base, infos: List[Info]) { def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors)) } def base_info(options: Options, session: String, progress: Progress = new Progress, dirs: List[Path] = Nil, include_sessions: List[String] = Nil, session_ancestor: Option[String] = None, session_requirements: Boolean = false): Base_Info = { val full_sessions = load_structure(options, dirs = dirs) val selected_sessions = full_sessions.selection(Selection(sessions = session :: session_ancestor.toList)) val info = selected_sessions(session) val ancestor = session_ancestor orElse info.parent val (session1, infos1) = if (session_requirements && ancestor.isDefined) { val deps = Sessions.deps(selected_sessions, progress = progress) val base = deps(session) val ancestor_loaded = deps.get(ancestor.get) match { case Some(ancestor_base) if !selected_sessions.imports_requirements(List(ancestor.get)).contains(session) => ancestor_base.loaded_theories.defined _ case _ => error("Bad ancestor " + quote(ancestor.get) + " for session " + quote(session)) } val required_theories = for { thy <- base.loaded_theories.keys if !ancestor_loaded(thy) && base.theory_qualifier(thy) != session } yield thy if (required_theories.isEmpty) (ancestor.get, Nil) else { val other_name = info.name + "_requirements(" + ancestor.get + ")" Isabelle_System.isabelle_tmp_prefix() (other_name, List( make_info(info.options, dir_selected = false, dir = Path.explode("$ISABELLE_TMP_PREFIX"), chapter = info.chapter, Session_Entry( pos = info.pos, name = other_name, groups = info.groups, path = ".", parent = ancestor, description = "Required theory imports from other sessions", options = Nil, imports = info.deps, directories = Nil, theories = List((Nil, required_theories.map(thy => ((thy, Position.none), false)))), document_files = Nil, export_files = Nil)))) } } else (session, Nil) val full_sessions1 = if (infos1.isEmpty) full_sessions else load_structure(options, dirs = dirs, infos = infos1) val selected_sessions1 = full_sessions1.selection(Selection(sessions = session1 :: session :: include_sessions)) val deps1 = Sessions.deps(selected_sessions1, progress = progress) Base_Info(session1, full_sessions1, deps1.errors, deps1(session1), infos1) } /* cumulative session info */ sealed case class Info( name: String, chapter: String, dir_selected: Boolean, pos: Position.T, groups: List[String], dir: Path, parent: Option[String], description: String, directories: List[Path], options: Options, imports: List[String], theories: List[(Options, List[(String, Position.T)])], global_theories: List[String], document_files: List[(Path, Path)], export_files: List[(Path, Int, List[String])], meta_digest: SHA1.Digest) { def deps: List[String] = parent.toList ::: imports def dirs: List[Path] = dir :: directories def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale")) def bibtex_entries: List[Text.Info[String]] = (for { (document_dir, file) <- document_files.iterator if Bibtex.is_bibtex(file.file_name) info <- Bibtex.entries(File.read(dir + document_dir + file)).iterator } yield info).toList def record_proofs: Boolean = options.int("record_proofs") >= 2 def is_afp: Boolean = chapter == AFP.chapter def is_afp_bulky: Boolean = is_afp && groups.exists(AFP.groups_bulky.contains) } def make_info(options: Options, dir_selected: Boolean, dir: Path, chapter: String, entry: Session_Entry): Info = { try { val name = entry.name if (exclude_session(name)) error("Bad session name") if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session") if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session") val session_path = dir + Path.explode(entry.path) val directories = entry.directories.map(dir => session_path + Path.explode(dir)) val session_options = options ++ entry.options val theories = entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map({ case ((thy, pos), _) => if (exclude_theory(thy)) error("Bad theory name " + quote(thy) + Position.here(pos)) else (thy, pos) })) }) val global_theories = for { (_, thys) <- entry.theories; ((thy, pos), global) <- thys if global } yield { val thy_name = Path.explode(thy).file_name if (Long_Name.is_qualified(thy_name)) error("Bad qualified name for global theory " + quote(thy_name) + Position.here(pos)) else thy_name } val conditions = theories.flatMap(thys => space_explode(',', thys._1.string("condition"))).distinct.sorted. map(x => (x, Isabelle_System.getenv(x) != "")) val document_files = entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) }) val export_files = entry.export_files.map({ case (dir, prune, pats) => (Path.explode(dir), prune, pats) }) val meta_digest = SHA1.digest((name, chapter, entry.parent, entry.directories, entry.options, entry.imports, entry.theories_no_position, conditions, entry.document_files).toString) Info(name, chapter, dir_selected, entry.pos, entry.groups, session_path, entry.parent, entry.description, directories, session_options, entry.imports, theories, global_theories, document_files, export_files, meta_digest) } catch { case ERROR(msg) => error(msg + "\nThe error(s) above occurred in session entry " + quote(entry.name) + Position.here(entry.pos)) } } object Selection { val empty: Selection = Selection() val all: Selection = Selection(all_sessions = true) def session(session: String): Selection = Selection(sessions = List(session)) } sealed case class Selection( requirements: Boolean = false, all_sessions: Boolean = false, base_sessions: List[String] = Nil, exclude_session_groups: List[String] = Nil, exclude_sessions: List[String] = Nil, session_groups: List[String] = Nil, sessions: List[String] = Nil) { def ++ (other: Selection): Selection = Selection( requirements = requirements || other.requirements, all_sessions = all_sessions || other.all_sessions, base_sessions = Library.merge(base_sessions, other.base_sessions), exclude_session_groups = Library.merge(exclude_session_groups, other.exclude_session_groups), exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions), session_groups = Library.merge(session_groups, other.session_groups), sessions = Library.merge(sessions, other.sessions)) } def make(infos: List[Info]): Structure = { def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String]) : Graph[String, Info] = { def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) = { if (!g.defined(parent)) error("Bad " + kind + " session " + quote(parent) + " for " + quote(name) + Position.here(pos)) try { g.add_edge_acyclic(parent, name) } catch { case exn: Graph.Cycles[_] => error(cat_lines(exn.cycles.map(cycle => "Cyclic session dependency of " + cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos)) } } (graph /: graph.iterator) { case (g, (name, (info, _))) => (g /: edges(info))(add_edge(info.pos, name, _, _)) } } val info_graph = (Graph.string[Info] /: infos) { case (graph, info) => if (graph.defined(info.name)) error("Duplicate session " + quote(info.name) + Position.here(info.pos) + Position.here(graph.get_node(info.name).pos)) else graph.new_node(info.name, info) } val build_graph = add_edges(info_graph, "parent", _.parent) val imports_graph = add_edges(build_graph, "imports", _.imports) val session_positions: List[(String, Position.T)] = (for ((name, (info, _)) <- info_graph.iterator) yield (name, info.pos)).toList val session_directories: Map[JFile, String] = (Map.empty[JFile, String] /: (for { session <- imports_graph.topological_order.iterator info = info_graph.get_node(session) dir <- info.dirs.iterator } yield (info, dir)))({ case (dirs, (info, dir)) => val session = info.name val canonical_dir = dir.canonical_file dirs.get(canonical_dir) match { case Some(session1) => val info1 = info_graph.get_node(session1) error("Duplicate use of directory " + dir + "\n for session " + quote(session1) + Position.here(info1.pos) + "\n vs. session " + quote(session) + Position.here(info.pos)) case None => dirs + (canonical_dir -> session) } }) val global_theories: Map[String, String] = (Thy_Header.bootstrap_global_theories.toMap /: (for { session <- imports_graph.topological_order.iterator info = info_graph.get_node(session) thy <- info.global_theories.iterator } yield (info, thy)))({ case (global, (info, thy)) => val qualifier = info.name global.get(thy) match { case Some(qualifier1) if qualifier != qualifier1 => error("Duplicate global theory " + quote(thy) + Position.here(info.pos)) case _ => global + (thy -> qualifier) } }) new Structure( session_positions, session_directories, global_theories, build_graph, imports_graph) } final class Structure private[Sessions]( val session_positions: List[(String, Position.T)], val session_directories: Map[JFile, String], val global_theories: Map[String, String], val build_graph: Graph[String, Info], val imports_graph: Graph[String, Info]) { sessions_structure => def dest_session_directories: List[(String, String)] = for ((file, session) <- session_directories.toList) yield (File.standard_path(file), session) lazy val chapters: SortedMap[String, List[Info]] = (SortedMap.empty[String, List[Info]] /: build_graph.iterator)( { case (chs, (_, (info, _))) => chs + (info.chapter -> (info :: chs.getOrElse(info.chapter, Nil))) }) def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph) def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph) def defined(name: String): Boolean = imports_graph.defined(name) def apply(name: String): Info = imports_graph.get_node(name) def get(name: String): Option[Info] = if (defined(name)) Some(apply(name)) else None def theory_qualifier(name: String): String = global_theories.getOrElse(name, Long_Name.qualifier(name)) def check_sessions(names: List[String]) { val bad_sessions = SortedSet(names.filterNot(defined): _*).toList if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions)) } def check_sessions(sel: Selection): Unit = check_sessions(sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions) private def selected(graph: Graph[String, Info], sel: Selection): List[String] = { check_sessions(sel) val select_group = sel.session_groups.toSet val select_session = sel.sessions.toSet ++ imports_graph.all_succs(sel.base_sessions) val selected0 = if (sel.all_sessions) graph.keys else { (for { (name, (info, _)) <- graph.iterator if info.dir_selected || select_session(name) || graph.get_node(name).groups.exists(select_group) } yield name).toList } if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList else selected0 } def selection(sel: Selection): Structure = { check_sessions(sel) val excluded = { val exclude_group = sel.exclude_session_groups.toSet val exclude_group_sessions = (for { (name, (info, _)) <- imports_graph.iterator if imports_graph.get_node(name).groups.exists(exclude_group) } yield name).toList imports_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet } def restrict(graph: Graph[String, Info]): Graph[String, Info] = { val sessions = graph.all_preds(selected(graph, sel)).filterNot(excluded) graph.restrict(graph.all_preds(sessions).toSet) } new Structure( session_positions, session_directories, global_theories, restrict(build_graph), restrict(imports_graph)) } def selection_deps( options: Options, selection: Selection, progress: Progress = new Progress, loading_sessions: Boolean = false, inlined_files: Boolean = false, verbose: Boolean = false): Deps = { val deps = Sessions.deps(sessions_structure.selection(selection), progress = progress, inlined_files = inlined_files, verbose = verbose) if (loading_sessions) { val selection_size = deps.sessions_structure.build_graph.size if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...") } deps } def build_selection(sel: Selection): List[String] = selected(build_graph, sel) def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss) - def build_requirements(ss: List[String]): List[String] = build_graph.all_preds(ss).reverse + def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss) def build_topological_order: List[String] = build_graph.topological_order def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel) def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss) - def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds(ss).reverse + def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss) def imports_topological_order: List[String] = imports_graph.topological_order override def toString: String = imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")") } /* parser */ val ROOT: Path = Path.explode("ROOT") val ROOTS: Path = Path.explode("ROOTS") private val CHAPTER = "chapter" private val SESSION = "session" private val IN = "in" private val DESCRIPTION = "description" private val DIRECTORIES = "directories" private val OPTIONS = "options" private val SESSIONS = "sessions" private val THEORIES = "theories" private val GLOBAL = "global" private val DOCUMENT_FILES = "document_files" private val EXPORT_FILES = "export_files" val root_syntax: Outer_Syntax = Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN + (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) + (DESCRIPTION, Keyword.QUASI_COMMAND) + (DIRECTORIES, Keyword.QUASI_COMMAND) + (OPTIONS, Keyword.QUASI_COMMAND) + (SESSIONS, Keyword.QUASI_COMMAND) + (THEORIES, Keyword.QUASI_COMMAND) + (DOCUMENT_FILES, Keyword.QUASI_COMMAND) + (EXPORT_FILES, Keyword.QUASI_COMMAND) abstract class Entry sealed case class Chapter(name: String) extends Entry sealed case class Session_Entry( pos: Position.T, name: String, groups: List[String], path: String, parent: Option[String], description: String, options: List[Options.Spec], imports: List[String], directories: List[String], theories: List[(List[Options.Spec], List[((String, Position.T), Boolean)])], document_files: List[(String, String)], export_files: List[(String, Int, List[String])]) extends Entry { def theories_no_position: List[(List[Options.Spec], List[(String, Boolean)])] = theories.map({ case (a, b) => (a, b.map({ case ((c, _), d) => (c, d) })) }) } private object Parser extends Options.Parser { private val chapter: Parser[Chapter] = { val chapter_name = atom("chapter name", _.is_name) command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) } } private val session_entry: Parser[Session_Entry] = { val option = option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) } val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]") val theory_entry = position(theory_name) ~ opt_keyword(GLOBAL) ^^ { case x ~ y => (x, y) } val theories = $$$(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_entry)) ^^ { case _ ~ (x ~ y) => (x, y) } val in_path = $$$("(") ~! ($$$(IN) ~ path ~ $$$(")")) ^^ { case _ ~ (_ ~ x ~ _) => x } val document_files = $$$(DOCUMENT_FILES) ~! ((in_path | success("document")) ~ rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) } val prune = $$$("[") ~! (nat ~ $$$("]")) ^^ { case _ ~ (x ~ _) => x } | success(0) val export_files = $$$(EXPORT_FILES) ~! ((in_path | success("export")) ~ prune ~ rep1(embedded)) ^^ { case _ ~ (x ~ y ~ z) => (x, y, z) } command(SESSION) ~! (position(session_name) ~ (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~ (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~ ($$$("=") ~! (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~ (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~ (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~ (($$$(SESSIONS) ~! rep1(session_name) ^^ { case _ ~ x => x }) | success(Nil)) ~ (($$$(DIRECTORIES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~ rep(theories) ~ (rep(document_files) ^^ (x => x.flatten)) ~ (rep(export_files))))) ^^ { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j ~ k))) => Session_Entry(pos, a, b, c, d, e, f, g, h, i, j, k) } } def parse_root(path: Path): List[Entry] = { val toks = Token.explode(root_syntax.keywords, File.read(path)) val start = Token.Pos.file(path.implode) parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match { case Success(result, _) => result case bad => error(bad.toString) } } } def parse_root(path: Path): List[Entry] = Parser.parse_root(path) def parse_root_entries(path: Path): List[Session_Entry] = for (entry <- Parser.parse_root(path) if entry.isInstanceOf[Session_Entry]) yield entry.asInstanceOf[Session_Entry] def read_root(options: Options, select: Boolean, path: Path): List[Info] = { var entry_chapter = UNSORTED val infos = new mutable.ListBuffer[Info] parse_root(path).foreach { case Chapter(name) => entry_chapter = name case entry: Session_Entry => infos += make_info(options, select, path.dir, entry_chapter, entry) } infos.toList } def parse_roots(roots: Path): List[String] = { for { line <- split_lines(File.read(roots)) if !(line == "" || line.startsWith("#")) } yield line } /* load sessions from certain directories */ private def is_session_dir(dir: Path): Boolean = (dir + ROOT).is_file || (dir + ROOTS).is_file private def check_session_dir(dir: Path): Path = if (is_session_dir(dir)) File.pwd() + dir.expand else error("Bad session root directory: " + dir.toString) def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] = { val default_dirs = Isabelle_System.components().filter(is_session_dir) for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) } yield (select, dir.canonical) } def load_structure(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, infos: List[Info] = Nil): Structure = { def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] = load_root(select, dir) ::: load_roots(select, dir) def load_root(select: Boolean, dir: Path): List[(Boolean, Path)] = { val root = dir + ROOT if (root.is_file) List((select, root)) else Nil } def load_roots(select: Boolean, dir: Path): List[(Boolean, Path)] = { val roots = dir + ROOTS if (roots.is_file) { for { entry <- parse_roots(roots) dir1 = try { check_session_dir(dir + Path.explode(entry)) } catch { case ERROR(msg) => error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString) } res <- load_dir(select, dir1) } yield res } else Nil } val roots = for { (select, dir) <- directories(dirs, select_dirs) res <- load_dir(select, check_session_dir(dir)) } yield res val unique_roots = ((Map.empty[JFile, (Boolean, Path)] /: roots) { case (m, (select, path)) => val file = path.canonical_file m.get(file) match { case None => m + (file -> (select, path)) case Some((select1, path1)) => m + (file -> (select1 || select, path1)) } }).toList.map(_._2) make(unique_roots.flatMap(p => read_root(options, p._1, p._2)) ::: infos) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("sessions", "explore structure of Isabelle sessions", 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 exclude_sessions: List[String] = Nil val getopts = Getopts(""" Usage: isabelle sessions [OPTIONS] [SESSIONS ...] Options are: -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -R refer to 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 -x NAME exclude session NAME and all descendants Explore the structure of Isabelle sessions and print result names in topological order (on stdout). """, "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)), "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) val sessions = getopts(args) val options = Options.init() val selection = 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) val sessions_structure = load_structure(options, dirs = dirs, select_dirs = select_dirs).selection(selection) for (name <- sessions_structure.imports_topological_order) { Output.writeln(name, stdout = true) } }) /** heap file with SHA1 digest **/ private val sha1_prefix = "SHA1:" def read_heap_digest(heap: Path): Option[String] = { if (heap.is_file) { using(FileChannel.open(heap.file.toPath, StandardOpenOption.READ))(file => { val len = file.size val n = sha1_prefix.length + SHA1.digest_length if (len >= n) { file.position(len - n) val buf = ByteBuffer.allocate(n) var i = 0 var m = 0 do { m = file.read(buf) if (m != -1) i += m } while (m != -1 && n > i) if (i == n) { val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset) val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset) if (prefix == sha1_prefix) Some(s) else None } else None } else None }) } else None } def write_heap_digest(heap: Path): String = read_heap_digest(heap) match { case None => val s = SHA1.digest(heap).rep File.append(heap, sha1_prefix + s) s case Some(s) => s } /** persistent store **/ object Session_Info { val session_name = SQL.Column.string("session_name").make_primary_key // Build_Log.Session_Info val session_timing = SQL.Column.bytes("session_timing") val command_timings = SQL.Column.bytes("command_timings") val theory_timings = SQL.Column.bytes("theory_timings") val ml_statistics = SQL.Column.bytes("ml_statistics") val task_statistics = SQL.Column.bytes("task_statistics") val errors = SQL.Column.bytes("errors") val build_log_columns = List(session_name, session_timing, command_timings, theory_timings, ml_statistics, task_statistics, errors) // Build.Session_Info val sources = SQL.Column.string("sources") val input_heaps = SQL.Column.string("input_heaps") val output_heap = SQL.Column.string("output_heap") val return_code = SQL.Column.int("return_code") val build_columns = List(sources, input_heaps, output_heap, return_code) val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns) } def store(options: Options): Store = new Store(options) class Store private[Sessions](val options: Options) { override def toString: String = "Store(output_dir = " + output_dir.expand + ")" val xml_cache: XML.Cache = XML.make_cache() val xz_cache: XZ.Cache = XZ.make_cache() /* directories */ val system_output_dir: Path = Path.explode("$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER") val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER") def system_heaps: Boolean = options.bool("system_heaps") val output_dir: Path = if (system_heaps) system_output_dir else user_output_dir val input_dirs: List[Path] = if (system_heaps) List(system_output_dir) else List(user_output_dir, system_output_dir) val browser_info: Path = if (system_heaps) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM") else Path.explode("$ISABELLE_BROWSER_INFO") /* file names */ def heap(name: String): Path = Path.basic(name) def database(name: String): Path = Path.basic("log") + Path.basic(name).ext("db") def log(name: String): Path = Path.basic("log") + Path.basic(name) def log_gz(name: String): Path = log(name).ext("gz") def output_heap(name: String): Path = output_dir + heap(name) def output_database(name: String): Path = output_dir + database(name) def output_log(name: String): Path = output_dir + log(name) def output_log_gz(name: String): Path = output_dir + log_gz(name) def prepare_output_dir() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) } /* heap */ def find_heap(name: String): Option[Path] = input_dirs.map(_ + heap(name)).find(_.is_file) def find_heap_digest(name: String): Option[String] = find_heap(name).flatMap(read_heap_digest) def the_heap(name: String): Path = find_heap(name) getOrElse error("Missing heap image for session " + quote(name) + " -- expected in:\n" + cat_lines(input_dirs.map(dir => " " + dir.expand.implode))) /* database */ private def database_server: Boolean = options.bool("build_database_server") def access_database(name: String, output: Boolean = false): Option[SQL.Database] = { if (database_server) { val db = PostgreSQL.open_database( user = options.string("build_database_user"), password = options.string("build_database_password"), database = options.string("build_database_name"), host = options.string("build_database_host"), port = options.int("build_database_port"), ssh = options.proper_string("build_database_ssh_host").map(ssh_host => SSH.open_session(options, host = ssh_host, user = options.string("build_database_ssh_user"), port = options.int("build_database_ssh_port"))), ssh_close = true) if (output || has_session_info(db, name)) Some(db) else { db.close; None } } else if (output) Some(SQLite.open_database(output_database(name))) else input_dirs.map(_ + database(name)).find(_.is_file).map(SQLite.open_database) } def open_database(name: String, output: Boolean = false): SQL.Database = access_database(name, output = output) getOrElse error("Missing build database for session " + quote(name)) def clean_output(name: String): (Boolean, Boolean) = { val relevant_db = database_server && { access_database(name) match { case Some(db) => try { db.transaction { val relevant_db = has_session_info(db, name) init_session_info(db, name) relevant_db } } finally { db.close } case None => false } } val del = for { dir <- (if (system_heaps) List(user_output_dir, system_output_dir) else List(user_output_dir)) file <- List(heap(name), database(name), log(name), log_gz(name)) path = dir + file if path.is_file } yield path.file.delete val relevant = relevant_db || del.nonEmpty val ok = del.forall(b => b) (relevant, ok) } /* SQL database content */ def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes = db.using_statement(Session_Info.table.select(List(column), Session_Info.session_name.where_equal(name)))(stmt => { val res = stmt.execute_query() if (!res.next()) Bytes.empty else res.bytes(column) }) def read_properties(db: SQL.Database, name: String, column: SQL.Column): List[Properties.T] = Properties.uncompress( read_bytes(db, name, column), cache = xz_cache, xml_cache = Some(xml_cache)) /* session info */ def init_session_info(db: SQL.Database, name: String) { db.transaction { db.create_table(Session_Info.table) db.using_statement( Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute) db.create_table(Export.Data.table) db.using_statement( Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute) } } def has_session_info(db: SQL.Database, name: String): Boolean = { db.transaction { db.tables.contains(Session_Info.table.name) && { db.using_statement( Session_Info.table.select(List(Session_Info.session_name), Session_Info.session_name.where_equal(name)))(stmt => stmt.execute_query().next()) } } } def write_session_info( db: SQL.Database, name: String, build_log: Build_Log.Session_Info, build: Build.Session_Info) { db.transaction { db.using_statement(Session_Info.table.insert())(stmt => { stmt.string(1) = name stmt.bytes(2) = Properties.encode(build_log.session_timing) stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = xz_cache) stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = xz_cache) stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = xz_cache) stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = xz_cache) stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = xz_cache) stmt.string(8) = build.sources stmt.string(9) = cat_lines(build.input_heaps) stmt.string(10) = build.output_heap getOrElse "" stmt.int(11) = build.return_code stmt.execute() }) } } def read_session_timing(db: SQL.Database, name: String): Properties.T = Properties.decode(read_bytes(db, name, Session_Info.session_timing), Some(xml_cache)) def read_command_timings(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.command_timings) def read_theory_timings(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.theory_timings) def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.ml_statistics) def read_task_statistics(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.task_statistics) def read_errors(db: SQL.Database, name: String): List[String] = Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = xz_cache) def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] = { if (db.tables.contains(Session_Info.table.name)) { db.using_statement(Session_Info.table.select(Session_Info.build_columns, Session_Info.session_name.where_equal(name)))(stmt => { val res = stmt.execute_query() if (!res.next()) None else { Some( Build.Session_Info( res.string(Session_Info.sources), split_lines(res.string(Session_Info.input_heaps)), res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) }, res.int(Session_Info.return_code))) } }) } else None } } } diff --git a/src/Pure/Tools/dump.scala b/src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala +++ b/src/Pure/Tools/dump.scala @@ -1,511 +1,511 @@ /* Title: Pure/Tools/dump.scala Author: Makarius Dump cumulative PIDE session database. */ package isabelle import java.io.{BufferedWriter, FileOutputStream, OutputStreamWriter} object Dump { /* aspects */ sealed case class Aspect_Args( options: Options, deps: Sessions.Deps, progress: Progress, output_dir: Path, snapshot: Document.Snapshot, status: Document_Status.Node_Status) { def write_path(file_name: Path): Path = { val path = output_dir + Path.basic(snapshot.node_name.theory) + file_name Isabelle_System.mkdirs(path.dir) path } def write(file_name: Path, bytes: Bytes): Unit = Bytes.write(write_path(file_name), bytes) def write(file_name: Path, text: String): Unit = write(file_name, Bytes(text)) def write(file_name: Path, body: XML.Body): Unit = using(File.writer(write_path(file_name).file))( writer => YXML.traversal(s => writer.write(Symbol.encode(s)), body)) } sealed case class Aspect(name: String, description: String, operation: Aspect_Args => Unit, options: List[String] = Nil) { override def toString: String = name } val known_aspects: List[Aspect] = List( Aspect("markup", "PIDE markup (YXML format)", { case args => args.write(Path.explode("markup.yxml"), args.snapshot.markup_to_XML(Text.Range.full, Markup.Elements.full)) }), Aspect("messages", "output messages (YXML format)", { case args => args.write(Path.explode("messages.yxml"), args.snapshot.messages.iterator.map(_._1).toList) }), Aspect("latex", "generated LaTeX source", { case args => for (entry <- args.snapshot.exports if entry.name == "document.tex") args.write(Path.explode(entry.name), entry.uncompressed()) }, options = List("export_document")), Aspect("theory", "foundational theory content", { case args => for { entry <- args.snapshot.exports if entry.name.startsWith(Export_Theory.export_prefix) } args.write(Path.explode(entry.name), entry.uncompressed()) }, options = List("export_theory")) ).sortBy(_.name) def show_aspects: String = cat_lines(known_aspects.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)) /* context and session */ sealed case class Args( session: Headless.Session, snapshot: Document.Snapshot, status: Document_Status.Node_Status) { def print_node: String = snapshot.node_name.toString } object Context { def apply( options: Options, aspects: List[Aspect] = Nil, progress: Progress = new Progress, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, selection: Sessions.Selection = Sessions.Selection.empty, pure_base: Boolean = false, skip_base: Boolean = false): Context = { val session_options: Options = { val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options val options1 = options0 + "ML_statistics=false" + "parallel_proofs=0" + "completion_limit=0" + "editor_tracing_messages=0" + "editor_presentation" (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) }) } val sessions_structure: Sessions.Structure = Sessions.load_structure(session_options, dirs = dirs, select_dirs = select_dirs). selection(selection) { val selection_size = sessions_structure.build_graph.size if (selection_size > 1) progress.echo("Loading " + selection_size + " sessions ...") } val deps: Sessions.Deps = Sessions.deps(sessions_structure, progress = progress).check_errors new Context(options, progress, dirs, select_dirs, pure_base, skip_base, session_options, deps) } } class Context private( val options: Options, val progress: Progress, val dirs: List[Path], val select_dirs: List[Path], val pure_base: Boolean, val skip_base: Boolean, val session_options: Options, val deps: Sessions.Deps) { context => def session_dirs: List[Path] = dirs ::: select_dirs def build_logic(logic: String) { Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = session_dirs, strict = true) } def sessions( logic: String = default_logic, log: Logger = No_Logger): List[Session] = { /* partitions */ def session_info(session_name: String): Sessions.Info = deps.sessions_structure(session_name) val session_graph = deps.sessions_structure.build_graph val all_sessions = session_graph.topological_order val afp_sessions = (for (name <- all_sessions if session_info(name).is_afp) yield name).toSet val afp_bulky_sessions = (for (name <- all_sessions if session_info(name).is_afp_bulky) yield name).toList val base_sessions = - session_graph.all_preds(List(logic).filter(session_graph.defined)).reverse + session_graph.all_preds_rev(List(logic).filter(session_graph.defined)) val proof_sessions = session_graph.all_succs( for (name <- all_sessions if session_info(name).record_proofs) yield name) /* resulting sessions */ def make_session( selected_sessions: List[String], session_logic: String = logic, strict: Boolean = false, record_proofs: Boolean = false): List[Session] = { if (selected_sessions.isEmpty && !strict) Nil else List(new Session(context, session_logic, log, selected_sessions, record_proofs)) } val PURE = isabelle.Thy_Header.PURE val base = if ((logic == PURE && !pure_base) || skip_base) Nil else make_session(base_sessions, session_logic = PURE, strict = logic == PURE) val main = make_session( session_graph.topological_order.filterNot(name => afp_sessions.contains(name) || base_sessions.contains(name) || proof_sessions.contains(name))) val proofs = make_session(proof_sessions, session_logic = PURE, record_proofs = true) val afp = if (afp_sessions.isEmpty) Nil else { val (part1, part2) = { val graph = session_graph.restrict(afp_sessions -- afp_bulky_sessions) val force_partition1 = AFP.force_partition1.filter(graph.defined) val force_part1 = graph.all_preds(graph.all_succs(force_partition1)).toSet graph.keys.partition(a => force_part1(a) || graph.is_isolated(a)) } List(part1, part2, afp_bulky_sessions).flatMap(make_session(_)) } proofs ::: base ::: main ::: afp } /* processed theories */ private val processed_theories = Synchronized(Set.empty[String]) def process_theory(theory: String): Boolean = processed_theories.change_result(processed => (!processed(theory), processed + theory)) /* errors */ private val errors = Synchronized(List.empty[String]) def add_errors(more_errs: List[String]) { errors.change(errs => errs ::: more_errs) } def check_errors { val errs = errors.value if (errs.nonEmpty) error(errs.mkString("\n\n")) } } class Session private[Dump]( val context: Context, val logic: String, log: Logger, selected_sessions: List[String], record_proofs: Boolean) { /* resources */ val options: Options = if (record_proofs) context.session_options + "record_proofs=2" else context.session_options private def deps = context.deps private def progress = context.progress val resources: Headless.Resources = Headless.Resources.make(options, logic, progress = progress, log = log, session_dirs = context.session_dirs, include_sessions = deps.sessions_structure.imports_topological_order) val used_theories: List[Document.Node.Name] = { for { session_name <- deps.sessions_structure.build_graph.restrict(selected_sessions.toSet).topological_order (name, theory_options) <- deps(session_name).used_theories if !resources.session_base.loaded_theory(name.theory) if { def warn(msg: String): Unit = progress.echo_warning("Skipping theory " + name + " (" + msg + ")") val conditions = space_explode(',', theory_options.string("condition")). filter(cond => Isabelle_System.getenv(cond) == "") if (conditions.nonEmpty) { warn("undefined " + conditions.mkString(", ")) false } else if (options.bool("skip_proofs") && !theory_options.bool("skip_proofs")) { warn("option skip_proofs") false } else true } } yield name } /* process */ def process(process_theory: Args => Unit, unicode_symbols: Boolean = false) { val session = resources.start_session(progress = progress) // asynchronous consumer object Consumer { sealed case class Bad_Theory( name: Document.Node.Name, status: Document_Status.Node_Status, errors: List[String]) private val consumer_bad_theories = Synchronized(List.empty[Bad_Theory]) private val consumer = Consumer_Thread.fork(name = "dump")( consume = (args: (Document.Snapshot, Document_Status.Node_Status)) => { val (snapshot, status) = args val name = snapshot.node_name if (status.ok) { try { if (context.process_theory(name.theory)) { process_theory(Args(session, snapshot, status)) } } catch { case exn: Throwable if !Exn.is_interrupt(exn) => val msg = Exn.message(exn) progress.echo("FAILED to process theory " + name) progress.echo_error_message(msg) consumer_bad_theories.change(Bad_Theory(name, status, List(msg)) :: _) } } else { val msgs = for ((tree, pos) <- snapshot.messages if Protocol.is_error(tree)) yield { "Error" + Position.here(pos) + ":\n" + XML.content(Pretty.formatted(List(tree))) } progress.echo("FAILED to process theory " + name) msgs.foreach(progress.echo_error_message) consumer_bad_theories.change(Bad_Theory(name, status, msgs) :: _) } true }) def apply(snapshot: Document.Snapshot, status: Document_Status.Node_Status): Unit = consumer.send((snapshot, status)) def shutdown(): List[Bad_Theory] = { consumer.shutdown() consumer_bad_theories.value.reverse } } // synchronous body try { val use_theories_result = session.use_theories(used_theories.map(_.theory), unicode_symbols = unicode_symbols, progress = progress, commit = Some(Consumer.apply)) val bad_theories = Consumer.shutdown() val bad_msgs = bad_theories.map(bad => Output.clean_yxml( "FAILED theory " + bad.name + (if (bad.status.consolidated) "" else ": " + bad.status.percentage + "% finished") + (if (bad.errors.isEmpty) "" else bad.errors.mkString("\n", "\n", "")))) val pending_msgs = use_theories_result.nodes_pending match { case Nil => Nil case pending => List("Pending theories: " + commas(pending.map(p => p._1.toString))) } context.add_errors(bad_msgs ::: pending_msgs) } finally { session.stop() } } } /* dump */ val default_output_dir: Path = Path.explode("dump") val default_logic: String = Thy_Header.PURE def dump( options: Options, logic: String, aspects: List[Aspect] = Nil, progress: Progress = new Progress, log: Logger = No_Logger, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, output_dir: Path = default_output_dir, selection: Sessions.Selection = Sessions.Selection.empty) { val context = Context(options, aspects = aspects, progress = progress, dirs = dirs, select_dirs = select_dirs, selection = selection) context.build_logic(logic) for (session <- context.sessions(logic = logic, log = log)) { session.process((args: Args) => { progress.echo("Processing theory " + args.print_node + " ...") val aspect_args = Aspect_Args(session.options, context.deps, progress, output_dir, args.snapshot, args.status) aspects.foreach(_.operation(aspect_args)) }) } context.check_errors } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("dump", "dump cumulative PIDE session database", args => { var aspects: List[Aspect] = known_aspects 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 var logic = default_logic var dirs: List[Path] = Nil var session_groups: List[String] = Nil var options = Options.init() var verbose = false var exclude_sessions: List[String] = Nil val getopts = Getopts(""" Usage: isabelle dump [OPTIONS] [SESSIONS ...] Options are: -A NAMES dump named aspects (default: """ + known_aspects.mkString("\"", ",", "\"") + """) -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 refer to requirements of selected sessions -X NAME exclude sessions from group NAME and all descendants -a select all sessions -b NAME base logic image (default """ + isabelle.quote(default_logic) + """) -d DIR include session directory -g NAME select session group NAME -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -v verbose -x NAME exclude session NAME and all descendants Dump cumulative PIDE session database, with the following aspects: """ + 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), "b:" -> (arg => logic = arg), "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), "g:" -> (arg => session_groups = session_groups ::: List(arg)), "o:" -> (arg => options = options + arg), "v" -> (_ => verbose = true), "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) val sessions = getopts(args) val progress = new Console_Progress(verbose = verbose) val start_date = Date.now() progress.echo_if(verbose, "Started at " + Build_Log.print_date(start_date)) progress.interrupt_handler { dump(options, logic, aspects = aspects, progress = progress, dirs = dirs, select_dirs = select_dirs, output_dir = output_dir, 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)) } val end_date = Date.now() val timing = end_date.time - start_date.time progress.echo_if(verbose, "\nFinished at " + Build_Log.print_date(end_date)) progress.echo(timing.message_hms + " elapsed time") }) }