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,342 +1,342 @@ /* 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 = entries.foldLeft(empty[Key, A](ord)) { case (graph, ((x, info), _)) => graph.new_node(x, info) } val graph2 = entries.foldLeft(graph1) { case (graph, ((x, _), ys)) => ys.foldLeft(graph) { 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 next(x).foldLeft(rs + (x -> length))(reach(length + count(x))) xs.foldLeft(Map.empty[Key, Long])(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 next(x).foldLeft((n + count(x), rs + 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)*/ 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) = if (rev) next(x).foldLeft((rs, r_set + x)) { case (b, a) => reach(a, b) } - else (next(x) :\ (rs, r_set + x))(reach) + else next(x).foldRight((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) } xs.foldLeft((List.empty[List[Key]], empty_keys))(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] = rep.foldLeft(List.empty[Key]) { case (ms, (m, (_, (preds, _)))) => if (preds.isEmpty) m :: ms else ms } def maximals: List[Key] = rep.foldLeft(List.empty[Key]) { 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]( succs.foldLeft(preds.foldLeft(rep - x)(del_adjacent(false, x)))(del_adjacent(true, x))) } def restrict(pred: Key => Boolean): Graph[Key, A] = iterator.foldLeft(this) { 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 irreducible_preds(x_set, path, z).foldLeft(ps)(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] = keys_iterator.foldLeft(this)(_.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] = xs.foldLeft(this)(_.add_edge_acyclic(_, y)) def topological_order: List[Key] = all_succs(minimals) } diff --git a/src/Pure/General/multi_map.scala b/src/Pure/General/multi_map.scala --- a/src/Pure/General/multi_map.scala +++ b/src/Pure/General/multi_map.scala @@ -1,91 +1,91 @@ /* Title: Pure/General/multi_map.scala Author: Makarius Maps with multiple entries per key. */ package isabelle import scala.collection.mutable import scala.collection.{IterableFactory, MapFactory, MapFactoryDefaults} import scala.collection.immutable.{Iterable, MapOps} object Multi_Map extends MapFactory[Multi_Map] { private val empty_val: Multi_Map[Any, Nothing] = new Multi_Map[Any, Nothing](Map.empty) def empty[A, B]: Multi_Map[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]] def from[A, B](entries: IterableOnce[(A, B)]): Multi_Map[A, B] = entries.foldLeft(empty[A, B]) { case (m, (a, b)) => m.insert(a, b) } override def newBuilder[A, B]: mutable.Builder[(A, B), Multi_Map[A, B]] = new Builder[A, B] private class Builder[A, B] extends mutable.Builder[(A, B), Multi_Map[A, B]] { private var res = empty[A, B] override def clear(): Unit = { res = empty[A, B] } override def addOne(p: (A, B)): this.type = { res = res.insert(p._1, p._2); this } override def result(): Multi_Map[A, B] = res } } final class Multi_Map[A, +B] private(protected val rep: Map[A, List[B]]) extends Iterable[(A, B)] with MapOps[A, B, Multi_Map, Multi_Map[A, B]] with MapFactoryDefaults[A, B, Multi_Map, Iterable] { /* Multi_Map operations */ def iterator_list: Iterator[(A, List[B])] = rep.iterator def get_list(a: A): List[B] = rep.getOrElse(a, Nil) def insert[B1 >: B](a: A, b: B1): Multi_Map[A, B1] = { val bs = get_list(a) if (bs.contains(b)) this else new Multi_Map(rep + (a -> (b :: bs))) } def remove[B1 >: B](a: A, b: B1): Multi_Map[A, B1] = { val bs = get_list(a) if (bs.contains(b)) { bs.filterNot(_ == b) match { case Nil => new Multi_Map(rep - a) case bs1 => new Multi_Map(rep + (a -> bs1)) } } else this } def ++[B1 >: B] (other: Multi_Map[A, B1]): Multi_Map[A, B1] = if (this eq other) this else if (isEmpty) other else other.rep.iterator.foldLeft(this.asInstanceOf[Multi_Map[A, B1]]) { - case (m1, (a, bs)) => (bs :\ m1) { case (b, m2) => m2.insert(a, b) } + case (m1, (a, bs)) => bs.foldRight(m1) { case (b, m2) => m2.insert(a, b) } } /* Map operations */ override def empty: Multi_Map[A, Nothing] = Multi_Map.empty override def isEmpty: Boolean = rep.isEmpty override def keySet: Set[A] = rep.keySet override def iterator: Iterator[(A, B)] = for ((a, bs) <- rep.iterator; b <- bs.iterator) yield (a, b) def get(a: A): Option[B] = get_list(a).headOption override def updated[B1 >: B](a: A, b: B1): Multi_Map[A, B1] = insert(a, b) override def removed(a: A): Multi_Map[A, B] = if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this override def mapFactory: MapFactory[Multi_Map] = Multi_Map override def toString: String = mkString("Multi_Map(", ", ", ")") } diff --git a/src/Pure/General/path.scala b/src/Pure/General/path.scala --- a/src/Pure/General/path.scala +++ b/src/Pure/General/path.scala @@ -1,306 +1,306 @@ /* Title: Pure/General/path.scala Author: Makarius Algebra of file-system paths: basic POSIX notation, extended by named roots (e.g. //foo) and variables (e.g. $BAR). */ package isabelle import java.io.{File => JFile} import scala.util.matching.Regex object Path { /* path elements */ sealed abstract class Elem private case class Root(name: String) extends Elem private case class Basic(name: String) extends Elem private case class Variable(name: String) extends Elem private case object Parent extends Elem private def err_elem(msg: String, s: String): Nothing = error(msg + " path element " + quote(s)) private val illegal_elem = Set("", "~", "~~", ".", "..") private val illegal_char = "/\\$:\"'<>|?*" private def check_elem(s: String): String = if (illegal_elem.contains(s)) err_elem("Illegal", s) else { for (c <- s) { if (c.toInt < 32) err_elem("Illegal control character " + c.toInt + " in", s) if (illegal_char.contains(c)) err_elem("Illegal character " + quote(c.toString) + " in", s) } s } private def root_elem(s: String): Elem = Root(check_elem(s)) private def basic_elem(s: String): Elem = Basic(check_elem(s)) private def variable_elem(s: String): Elem = Variable(check_elem(s)) private def apply_elem(y: Elem, xs: List[Elem]): List[Elem] = (y, xs) match { case (Root(_), _) => List(y) case (Parent, Root(_) :: _) => xs case (Parent, Basic(_) :: rest) => rest case _ => y :: xs } private def norm_elems(elems: List[Elem]): List[Elem] = - (elems :\ (Nil: List[Elem]))(apply_elem) + elems.foldRight(Nil: List[Elem])(apply_elem) private def implode_elem(elem: Elem, short: Boolean): String = elem match { case Root("") => "" case Root(s) => "//" + s case Basic(s) => s case Variable("USER_HOME") if short => "~" case Variable("ISABELLE_HOME") if short => "~~" case Variable(s) => "$" + s case Parent => ".." } private def squash_elem(elem: Elem): String = elem match { case Root("") => "ROOT" case Root(s) => "SERVER_" + s case Basic(s) => s case Variable(s) => s case Parent => "PARENT" } /* path constructors */ val current: Path = new Path(Nil) val root: Path = new Path(List(Root(""))) def named_root(s: String): Path = new Path(List(root_elem(s))) def make(elems: List[String]): Path = new Path(elems.reverse.map(basic_elem)) def basic(s: String): Path = new Path(List(basic_elem(s))) def variable(s: String): Path = new Path(List(variable_elem(s))) val parent: Path = new Path(List(Parent)) /* explode */ def explode(str: String): Path = { def explode_elem(s: String): Elem = try { if (s == "..") Parent else if (s == "~") Variable("USER_HOME") else if (s == "~~") Variable("ISABELLE_HOME") else if (s.startsWith("$")) variable_elem(s.substring(1)) else basic_elem(s) } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in " + quote(str)) } val ss = space_explode('/', str) val r = ss.takeWhile(_.isEmpty).length val es = ss.dropWhile(_.isEmpty) val (roots, raw_elems) = if (r == 0) (Nil, es) else if (r == 1) (List(Root("")), es) else if (es.isEmpty) (List(Root("")), Nil) else (List(root_elem(es.head)), es.tail) val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem) new Path(norm_elems(elems reverse_::: roots)) } def is_wellformed(str: String): Boolean = try { explode(str); true } catch { case ERROR(_) => false } def is_valid(str: String): Boolean = try { explode(str).expand; true } catch { case ERROR(_) => false } def split(str: String): List[Path] = space_explode(':', str).filterNot(_.isEmpty).map(explode) /* encode */ val encode: XML.Encode.T[Path] = (path => XML.Encode.string(path.implode)) /* reserved names */ private val reserved_windows: Set[String] = Set("CON", "PRN", "AUX", "NUL", "COM1", "COM2", "COM3", "COM4", "COM5", "COM6", "COM7", "COM8", "COM9", "LPT1", "LPT2", "LPT3", "LPT4", "LPT5", "LPT6", "LPT7", "LPT8", "LPT9") def is_reserved(name: String): Boolean = Long_Name.explode(name).exists(a => reserved_windows.contains(Word.uppercase(a))) /* case-insensitive names */ def check_case_insensitive(paths: List[Path]): Unit = { val table = paths.foldLeft(Multi_Map.empty[String, String]) { case (tab, path) => val name = path.expand.implode tab.insert(Word.lowercase(name), name) } val collisions = (for { (_, coll) <- table.iterator_list if coll.length > 1 } yield coll).toList.flatten if (collisions.nonEmpty) { error(("Collision of file names due case-insensitivity:" :: collisions).mkString("\n ")) } } } final class Path private(protected val elems: List[Path.Elem]) // reversed elements { override def hashCode: Int = elems.hashCode override def equals(that: Any): Boolean = that match { case other: Path => elems == other.elems case _ => false } def is_current: Boolean = elems.isEmpty def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root] def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false } def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false } def starts_basic: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Basic] - def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem)) + def +(other: Path): Path = new Path(other.elems.foldRight(elems)(Path.apply_elem)) /* implode */ private def gen_implode(short: Boolean): String = elems match { case Nil => "." case List(Path.Root("")) => "/" case _ => elems.map(Path.implode_elem(_, short)).reverse.mkString("/") } def implode: String = gen_implode(false) def implode_short: String = gen_implode(true) override def toString: String = quote(implode) /* base element */ private def split_path: (Path, String) = elems match { case Path.Basic(s) :: xs => (new Path(xs), s) case _ => error("Cannot split path into dir/base: " + toString) } def dir: Path = split_path._1 def base: Path = new Path(List(Path.Basic(split_path._2))) def ext(e: String): Path = if (e == "") this else { val (prfx, s) = split_path prfx + Path.basic(s + "." + e) } def xz: Path = ext("xz") def html: Path = ext("html") def tex: Path = ext("tex") def pdf: Path = ext("pdf") def thy: Path = ext("thy") def backup: Path = { val (prfx, s) = split_path prfx + Path.basic(s + "~") } def backup2: Path = { val (prfx, s) = split_path prfx + Path.basic(s + "~~") } def platform_exe: Path = if (Platform.is_windows) ext("exe") else this private val Ext = new Regex("(.*)\\.([^.]*)") def split_ext: (Path, String) = { val (prefix, base) = split_path base match { case Ext(b, e) => (prefix + Path.basic(b), e) case _ => (prefix + Path.basic(base), "") } } def drop_ext: Path = split_ext._1 def get_ext: String = split_ext._2 def squash: Path = new Path(elems.map(elem => Path.Basic(Path.squash_elem(elem)))) /* expand */ def expand_env(env: Map[String, String]): Path = { def eval(elem: Path.Elem): List[Path.Elem] = elem match { case Path.Variable(s) => val path = Path.explode(Isabelle_System.getenv_strict(s, env)) if (path.elems.exists(_.isInstanceOf[Path.Variable])) error("Illegal path variable nesting: " + s + "=" + path.toString) else path.elems case x => List(x) } new Path(Path.norm_elems(elems.flatMap(eval))) } def expand: Path = expand_env(Isabelle_System.settings()) def file_name: String = expand.base.implode /* implode wrt. given directories */ def implode_symbolic: String = { val directories = Library.space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse val full_name = expand.implode directories.view.flatMap(a => try { val b = Path.explode(a).expand.implode if (full_name == b) Some(a) else { Library.try_unprefix(b + "/", full_name) match { case Some(name) => Some(a + "/" + name) case None => None } } } catch { case ERROR(_) => None }).headOption.getOrElse(implode) } def position: Position.T = Position.File(implode_symbolic) /* platform files */ def file: JFile = File.platform_file(this) def is_file: Boolean = file.isFile def is_dir: Boolean = file.isDirectory def absolute_file: JFile = File.absolute(file) def canonical_file: JFile = File.canonical(file) def absolute: Path = File.path(absolute_file) def canonical: Path = File.path(canonical_file) } diff --git a/src/Pure/PIDE/markup.scala b/src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala +++ b/src/Pure/PIDE/markup.scala @@ -1,740 +1,740 @@ /* Title: Pure/PIDE/markup.scala Author: Makarius Quasi-abstract markup elements. */ package isabelle object Markup { /* elements */ object Elements { def apply(elems: Set[String]): Elements = new Elements(elems) def apply(elems: String*): Elements = apply(Set(elems: _*)) val empty: Elements = apply() val full: Elements = new Elements(Set.empty) { override def apply(elem: String): Boolean = true override def toString: String = "Elements.full" } } sealed class Elements private[Markup](private val rep: Set[String]) { def apply(elem: String): Boolean = rep.contains(elem) def + (elem: String): Elements = new Elements(rep + elem) def ++ (elems: Elements): Elements = new Elements(rep ++ elems.rep) def - (elem: String): Elements = new Elements(rep - elem) def -- (elems: Elements): Elements = new Elements(rep -- elems.rep) override def toString: String = rep.mkString("Elements(", ",", ")") } /* properties */ val NAME = "name" val Name = new Properties.String(NAME) val XNAME = "xname" val XName = new Properties.String(XNAME) val KIND = "kind" val Kind = new Properties.String(KIND) val CONTENT = "content" val Content = new Properties.String(CONTENT) val SERIAL = "serial" val Serial = new Properties.Long(SERIAL) val INSTANCE = "instance" val Instance = new Properties.String(INSTANCE) /* basic markup */ val Empty: Markup = Markup("", Nil) val Broken: Markup = Markup("broken", Nil) class Markup_String(val name: String, prop: String) { private val Prop = new Properties.String(prop) def apply(s: String): Markup = Markup(name, Prop(s)) def unapply(markup: Markup): Option[String] = if (markup.name == name) Prop.unapply(markup.properties) else None } class Markup_Int(val name: String, prop: String) { private val Prop = new Properties.Int(prop) def apply(i: Int): Markup = Markup(name, Prop(i)) def unapply(markup: Markup): Option[Int] = if (markup.name == name) Prop.unapply(markup.properties) else None } class Markup_Long(val name: String, prop: String) { private val Prop = new Properties.Long(prop) def apply(i: Long): Markup = Markup(name, Prop(i)) def unapply(markup: Markup): Option[Long] = if (markup.name == name) Prop.unapply(markup.properties) else None } /* meta data */ val META_TITLE = "meta_title" val META_CREATOR = "meta_creator" val META_CONTRIBUTOR = "meta_contributor" val META_DATE = "meta_date" val META_LICENSE = "meta_license" val META_DESCRIPTION = "meta_description" /* formal entities */ val BINDING = "binding" val ENTITY = "entity" val Def = new Properties.Long("def") val Ref = new Properties.Long("ref") object Entity { object Def { def unapply(markup: Markup): Option[Long] = if (markup.name == ENTITY) Markup.Def.unapply(markup.properties) else None } object Ref { def unapply(markup: Markup): Option[Long] = if (markup.name == ENTITY) Markup.Ref.unapply(markup.properties) else None } object Occ { def unapply(markup: Markup): Option[Long] = Def.unapply(markup) orElse Ref.unapply(markup) } def unapply(markup: Markup): Option[(String, String)] = markup match { case Markup(ENTITY, props) => val kind = Kind.unapply(props).getOrElse("") val name = Name.unapply(props).getOrElse("") Some((kind, name)) case _ => None } } /* completion */ val COMPLETION = "completion" val NO_COMPLETION = "no_completion" val UPDATE = "update" /* position */ val LINE = "line" val END_LINE = "line" val OFFSET = "offset" val END_OFFSET = "end_offset" val FILE = "file" val ID = "id" val DEF_LINE = "def_line" val DEF_OFFSET = "def_offset" val DEF_END_OFFSET = "def_end_offset" val DEF_FILE = "def_file" val DEF_ID = "def_id" val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID) def position_property(entry: Properties.Entry): Boolean = POSITION_PROPERTIES(entry._1) val POSITION = "position" /* expression */ val EXPRESSION = "expression" object Expression { def unapply(markup: Markup): Option[String] = markup match { case Markup(EXPRESSION, Kind(kind)) => Some(kind) case Markup(EXPRESSION, _) => Some("") case _ => None } } /* citation */ val CITATION = "citation" val Citation = new Markup_String(CITATION, NAME) /* embedded languages */ val Symbols = new Properties.Boolean("symbols") val Antiquotes = new Properties.Boolean("antiquotes") val Delimited = new Properties.Boolean("delimited") val LANGUAGE = "language" object Language { val DOCUMENT = "document" val ML = "ML" val SML = "SML" val PATH = "path" val UNKNOWN = "unknown" def unapply(markup: Markup): Option[(String, Boolean, Boolean, Boolean)] = markup match { case Markup(LANGUAGE, props) => (props, props, props, props) match { case (Name(name), Symbols(symbols), Antiquotes(antiquotes), Delimited(delimited)) => Some((name, symbols, antiquotes, delimited)) case _ => None } case _ => None } object Path { def unapply(markup: Markup): Option[Boolean] = markup match { case Language(PATH, _, _, delimited) => Some(delimited) case _ => None } } } /* external resources */ val PATH = "path" val Path = new Markup_String(PATH, NAME) val EXPORT_PATH = "export_path" val Export_Path = new Markup_String(EXPORT_PATH, NAME) val URL = "url" val Url = new Markup_String(URL, NAME) val DOC = "doc" val Doc = new Markup_String(DOC, NAME) /* pretty printing */ val Consistent = new Properties.Boolean("consistent") val Indent = new Properties.Int("indent") val Width = new Properties.Int("width") object Block { val name = "block" def apply(c: Boolean, i: Int): Markup = Markup(name, (if (c) Consistent(c) else Nil) ::: (if (i != 0) Indent(i) else Nil)) def unapply(markup: Markup): Option[(Boolean, Int)] = if (markup.name == name) { val c = Consistent.unapply(markup.properties).getOrElse(false) val i = Indent.unapply(markup.properties).getOrElse(0) Some((c, i)) } else None } object Break { val name = "break" def apply(w: Int, i: Int): Markup = Markup(name, (if (w != 0) Width(w) else Nil) ::: (if (i != 0) Indent(i) else Nil)) def unapply(markup: Markup): Option[(Int, Int)] = if (markup.name == name) { val w = Width.unapply(markup.properties).getOrElse(0) val i = Indent.unapply(markup.properties).getOrElse(0) Some((w, i)) } else None } val ITEM = "item" val BULLET = "bullet" val SEPARATOR = "separator" /* text properties */ val WORDS = "words" val HIDDEN = "hidden" val DELETE = "delete" /* misc entities */ val THEORY = "theory" val CLASS = "class" val TYPE_NAME = "type_name" val FIXED = "fixed" val CASE = "case" val CONSTANT = "constant" val DYNAMIC_FACT = "dynamic_fact" /* inner syntax */ val TFREE = "tfree" val TVAR = "tvar" val FREE = "free" val SKOLEM = "skolem" val BOUND = "bound" val VAR = "var" val NUMERAL = "numeral" val LITERAL = "literal" val DELIMITER = "delimiter" val INNER_STRING = "inner_string" val INNER_CARTOUCHE = "inner_cartouche" val TOKEN_RANGE = "token_range" val SORTING = "sorting" val TYPING = "typing" val CLASS_PARAMETER = "class_parameter" val ATTRIBUTE = "attribute" val METHOD = "method" /* antiquotations */ val ANTIQUOTED = "antiquoted" val ANTIQUOTE = "antiquote" val ML_ANTIQUOTATION = "ML_antiquotation" val DOCUMENT_ANTIQUOTATION = "document_antiquotation" val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option" /* document text */ val RAW_TEXT = "raw_text" val PLAIN_TEXT = "plain_text" val PARAGRAPH = "paragraph" val TEXT_FOLD = "text_fold" object Document_Tag { val ELEMENT = "document_tag" val IMPORTANT = "important" val UNIMPORTANT = "unimportant" def unapply(markup: Markup): Option[String] = markup match { case Markup(ELEMENT, Name(name)) => Some(name) case _ => None } } /* Markdown document structure */ val MARKDOWN_PARAGRAPH = "markdown_paragraph" val MARKDOWN_ITEM = "markdown_item" val Markdown_Bullet = new Markup_Int("markdown_bullet", "depth") val Markdown_List = new Markup_String("markdown_list", "kind") val ITEMIZE = "itemize" val ENUMERATE = "enumerate" val DESCRIPTION = "description" /* ML */ val ML_KEYWORD1 = "ML_keyword1" val ML_KEYWORD2 = "ML_keyword2" val ML_KEYWORD3 = "ML_keyword3" val ML_DELIMITER = "ML_delimiter" val ML_TVAR = "ML_tvar" val ML_NUMERAL = "ML_numeral" val ML_CHAR = "ML_char" val ML_STRING = "ML_string" val ML_COMMENT = "ML_comment" val ML_DEF = "ML_def" val ML_OPEN = "ML_open" val ML_STRUCTURE = "ML_structure" val ML_TYPING = "ML_typing" val ML_BREAKPOINT = "ML_breakpoint" /* outer syntax */ val COMMAND = "command" val KEYWORD = "keyword" val KEYWORD1 = "keyword1" val KEYWORD2 = "keyword2" val KEYWORD3 = "keyword3" val QUASI_KEYWORD = "quasi_keyword" val IMPROPER = "improper" val OPERATOR = "operator" val STRING = "string" val ALT_STRING = "alt_string" val VERBATIM = "verbatim" val CARTOUCHE = "cartouche" val COMMENT = "comment" val LOAD_COMMAND = "load_command" /* comments */ val COMMENT1 = "comment1" val COMMENT2 = "comment2" val COMMENT3 = "comment3" /* timing */ val Elapsed = new Properties.Double("elapsed") val CPU = new Properties.Double("cpu") val GC = new Properties.Double("gc") object Timing_Properties { def apply(timing: isabelle.Timing): Properties.T = Elapsed(timing.elapsed.seconds) ::: CPU(timing.cpu.seconds) ::: GC(timing.gc.seconds) def unapply(props: Properties.T): Option[isabelle.Timing] = (props, props, props) match { case (Elapsed(elapsed), CPU(cpu), GC(gc)) => Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc))) case _ => None } def parse(props: Properties.T): isabelle.Timing = unapply(props) getOrElse isabelle.Timing.zero } val TIMING = "timing" object Timing { def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing)) def unapply(markup: Markup): Option[isabelle.Timing] = markup match { case Markup(TIMING, Timing_Properties(timing)) => Some(timing) case _ => None } } /* process result */ val Return_Code = new Properties.Int("return_code") object Process_Result { def apply(result: Process_Result): Properties.T = Return_Code(result.rc) ::: (if (result.timing.is_zero) Nil else Timing_Properties(result.timing)) def unapply(props: Properties.T): Option[Process_Result] = props match { case Return_Code(rc) => val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero) Some(isabelle.Process_Result(rc, timing = timing)) case _ => None } } /* command indentation */ object Command_Indent { val name = "command_indent" def unapply(markup: Markup): Option[Int] = if (markup.name == name) Indent.unapply(markup.properties) else None } /* goals */ val GOAL = "goal" val SUBGOAL = "subgoal" /* command status */ val TASK = "task" val ACCEPTED = "accepted" val FORKED = "forked" val JOINED = "joined" val RUNNING = "running" val FINISHED = "finished" val FAILED = "failed" val CANCELED = "canceled" val INITIALIZED = "initialized" val FINALIZED = "finalized" val CONSOLIDATING = "consolidating" val CONSOLIDATED = "consolidated" /* interactive documents */ val VERSION = "version" val ASSIGN = "assign" /* prover process */ val PROVER_COMMAND = "prover_command" val PROVER_ARG = "prover_arg" /* messages */ val INIT = "init" val STATUS = "status" val REPORT = "report" val RESULT = "result" val WRITELN = "writeln" val STATE = "state" val INFORMATION = "information" val TRACING = "tracing" val WARNING = "warning" val LEGACY = "legacy" val ERROR = "error" val NODES_STATUS = "nodes_status" val PROTOCOL = "protocol" val SYSTEM = "system" val STDOUT = "stdout" val STDERR = "stderr" val EXIT = "exit" val WRITELN_MESSAGE = "writeln_message" val STATE_MESSAGE = "state_message" val INFORMATION_MESSAGE = "information_message" val TRACING_MESSAGE = "tracing_message" val WARNING_MESSAGE = "warning_message" val LEGACY_MESSAGE = "legacy_message" val ERROR_MESSAGE = "error_message" val messages = Map( WRITELN -> WRITELN_MESSAGE, STATE -> STATE_MESSAGE, INFORMATION -> INFORMATION_MESSAGE, TRACING -> TRACING_MESSAGE, WARNING -> WARNING_MESSAGE, LEGACY -> LEGACY_MESSAGE, ERROR -> ERROR_MESSAGE) val message: String => String = messages.withDefault((s: String) => s) val NO_REPORT = "no_report" val BAD = "bad" val INTENSIFY = "intensify" /* active areas */ val BROWSER = "browser" val GRAPHVIEW = "graphview" val THEORY_EXPORTS = "theory_exports" val SENDBACK = "sendback" val PADDING = "padding" val PADDING_LINE = (PADDING, "line") val PADDING_COMMAND = (PADDING, "command") val DIALOG = "dialog" val Result = new Properties.String(RESULT) val JEDIT_ACTION = "jedit_action" /* protocol message functions */ val FUNCTION = "function" class Function(val name: String) { val PROPERTY: Properties.Entry = (FUNCTION, name) } class Properties_Function(name: String) extends Function(name) { def unapply(props: Properties.T): Option[Properties.T] = props match { case PROPERTY :: args => Some(args) case _ => None } } class Name_Function(name: String) extends Function(name) { def unapply(props: Properties.T): Option[String] = props match { case List(PROPERTY, (NAME, a)) => Some(a) case _ => None } } object ML_Statistics extends Function("ML_statistics") { def unapply(props: Properties.T): Option[(Long, String)] = props match { case List(PROPERTY, ("pid", Value.Long(pid)), ("stats_dir", stats_dir)) => Some((pid, stats_dir)) case _ => None } } val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name) def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1) object Command_Timing extends Properties_Function("command_timing") object Theory_Timing extends Properties_Function("theory_timing") object Session_Timing extends Properties_Function("session_timing") { val Threads = new Properties.Int("threads") } object Task_Statistics extends Properties_Function("task_statistics") object Loading_Theory extends Properties_Function("loading_theory") object Build_Session_Finished extends Function("build_session_finished") object Commands_Accepted extends Function("commands_accepted") object Assign_Update extends Function("assign_update") object Removed_Versions extends Function("removed_versions") object Invoke_Scala extends Function("invoke_scala") { def unapply(props: Properties.T): Option[(String, String, Boolean)] = props match { case List(PROPERTY, (NAME, name), (ID, id), ("thread", Value.Boolean(thread))) => Some((name, id, thread)) case _ => None } } object Cancel_Scala extends Function("cancel_scala") { def unapply(props: Properties.T): Option[String] = props match { case List(PROPERTY, (ID, id)) => Some(id) case _ => None } } val PRINT_OPERATIONS = "print_operations" /* export */ val EXPORT = "export" val THEORY_NAME = "theory_name" val EXECUTABLE = "executable" val COMPRESS = "compress" val STRICT = "strict" /* debugger output */ val DEBUGGER_STATE = "debugger_state" object Debugger_State { def unapply(props: Properties.T): Option[String] = props match { case List((FUNCTION, DEBUGGER_STATE), (NAME, name)) => Some(name) case _ => None } } val DEBUGGER_OUTPUT = "debugger_output" object Debugger_Output { def unapply(props: Properties.T): Option[String] = props match { case List((FUNCTION, DEBUGGER_OUTPUT), (NAME, name)) => Some(name) case _ => None } } /* simplifier trace */ val SIMP_TRACE_PANEL = "simp_trace_panel" val SIMP_TRACE_LOG = "simp_trace_log" val SIMP_TRACE_STEP = "simp_trace_step" val SIMP_TRACE_RECURSE = "simp_trace_recurse" val SIMP_TRACE_HINT = "simp_trace_hint" val SIMP_TRACE_IGNORE = "simp_trace_ignore" val SIMP_TRACE_CANCEL = "simp_trace_cancel" object Simp_Trace_Cancel { def unapply(props: Properties.T): Option[Long] = props match { case (FUNCTION, SIMP_TRACE_CANCEL) :: Serial(i) => Some(i) case _ => None } } /* XML data representation */ def encode: XML.Encode.T[Markup] = (markup: Markup) => { import XML.Encode._ pair(string, properties)((markup.name, markup.properties)) } def decode: XML.Decode.T[Markup] = (body: XML.Body) => { import XML.Decode._ val (name, props) = pair(string, properties)(body) Markup(name, props) } } sealed case class Markup(name: String, properties: Properties.T) { def markup(s: String): String = YXML.string_of_tree(XML.Elem(this, List(XML.Text(s)))) def update_properties(more_props: Properties.T): Markup = if (more_props.isEmpty) this - else Markup(name, (more_props :\ properties) { case (p, ps) => Properties.put(ps, p) }) + else Markup(name, more_props.foldRight(properties) { case (p, ps) => Properties.put(ps, p) }) def + (entry: Properties.Entry): Markup = Markup(name, Properties.put(properties, entry)) }