diff --git a/src/Pure/General/linear_set.scala b/src/Pure/General/linear_set.scala --- a/src/Pure/General/linear_set.scala +++ b/src/Pure/General/linear_set.scala @@ -1,164 +1,165 @@ /* Title: Pure/General/linear_set.scala Author: Makarius Author: Fabian Immler, TU Munich Sets with canonical linear order, or immutable linked-lists. */ package isabelle import scala.collection.mutable import scala.collection.immutable.SetOps import scala.collection.{IterableFactory, IterableFactoryDefaults} object Linear_Set extends IterableFactory[Linear_Set] { private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map()) override def empty[A]: Linear_Set[A] = empty_val.asInstanceOf[Linear_Set[A]] - def from[A](entries: IterableOnce[A]): Linear_Set[A] = entries.foldLeft(empty[A])(_.incl(_)) + def from[A](entries: IterableOnce[A]): Linear_Set[A] = + entries.iterator.foldLeft(empty[A])(_.incl(_)) override def newBuilder[A]: mutable.Builder[A, Linear_Set[A]] = new Builder[A] private class Builder[A] extends mutable.Builder[A, Linear_Set[A]] { private var res = empty[A] override def clear(): Unit = { res = empty[A] } override def addOne(elem: A): this.type = { res = res.incl(elem); this } override def result(): Linear_Set[A] = res } class Duplicate[A](x: A) extends Exception class Undefined[A](x: A) extends Exception class Next_Undefined[A](x: Option[A]) extends Exception } final class Linear_Set[A] private( start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A]) extends Iterable[A] with SetOps[A, Linear_Set, Linear_Set[A]] with IterableFactoryDefaults[A, Linear_Set] { /* relative addressing */ def next(elem: A): Option[A] = if (contains(elem)) nexts.get(elem) else throw new Linear_Set.Undefined(elem) def prev(elem: A): Option[A] = if (contains(elem)) prevs.get(elem) else throw new Linear_Set.Undefined(elem) def get_after(hook: Option[A]): Option[A] = hook match { case None => start case Some(elem) => next(elem) } def insert_after(hook: Option[A], elem: A): Linear_Set[A] = if (contains(elem)) throw new Linear_Set.Duplicate(elem) else hook match { case None => start match { case None => new Linear_Set[A](Some(elem), Some(elem), Map(), Map()) case Some(elem1) => new Linear_Set[A](Some(elem), end, nexts + (elem -> elem1), prevs + (elem1 -> elem)) } case Some(elem1) => if (!contains(elem1)) throw new Linear_Set.Undefined(elem1) else nexts.get(elem1) match { case None => new Linear_Set[A](start, Some(elem), nexts + (elem1 -> elem), prevs + (elem -> elem1)) case Some(elem2) => new Linear_Set[A](start, end, nexts + (elem1 -> elem) + (elem -> elem2), prevs + (elem2 -> elem) + (elem -> elem1)) } } def append_after(hook: Option[A], elems: Iterable[A]): Linear_Set[A] = // FIXME reverse fold elems.foldLeft((hook, this)) { case ((last, set), elem) => (Some(elem), set.insert_after(last, elem)) }._2 def delete_after(hook: Option[A]): Linear_Set[A] = hook match { case None => start match { case None => throw new Linear_Set.Next_Undefined[A](None) case Some(elem1) => nexts.get(elem1) match { case None => empty case Some(elem2) => new Linear_Set[A](Some(elem2), end, nexts - elem1, prevs - elem2) } } case Some(elem1) => if (!contains(elem1)) throw new Linear_Set.Undefined(elem1) else nexts.get(elem1) match { case None => throw new Linear_Set.Next_Undefined(Some(elem1)) case Some(elem2) => nexts.get(elem2) match { case None => new Linear_Set[A](start, Some(elem1), nexts - elem1, prevs - elem2) case Some(elem3) => new Linear_Set[A](start, end, nexts - elem2 + (elem1 -> elem3), prevs - elem2 + (elem3 -> elem1)) } } } /* Set methods */ override def isEmpty: Boolean = start.isEmpty override def size: Int = if (isEmpty) 0 else nexts.size + 1 def contains(elem: A): Boolean = nonEmpty && (end.get == elem || nexts.isDefinedAt(elem)) private def make_iterator(from: Option[A]): Iterator[A] = new Iterator[A] { private var next_elem = from def hasNext: Boolean = next_elem.isDefined def next(): A = next_elem match { case Some(elem) => next_elem = nexts.get(elem) elem case None => Iterator.empty.next() } } override def iterator: Iterator[A] = make_iterator(start) def iterator(elem: A): Iterator[A] = if (contains(elem)) make_iterator(Some(elem)) else throw new Linear_Set.Undefined(elem) def iterator(from: A, to: A): Iterator[A] = if (contains(to)) nexts.get(to) match { case None => iterator(from) case Some(stop) => iterator(from).takeWhile(_ != stop) } else throw new Linear_Set.Undefined(to) def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts) override def last: A = reverse.head def incl(elem: A): Linear_Set[A] = insert_after(end, elem) def excl(elem: A): Linear_Set[A] = delete_after(prev(elem)) override def iterableFactory: IterableFactory[Linear_Set] = Linear_Set override def toString: String = mkString("Linear_Set(", ", ", ")") } 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) } + entries.iterator.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.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/scan.scala b/src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala +++ b/src/Pure/General/scan.scala @@ -1,511 +1,512 @@ /* Title: Pure/General/scan.scala Author: Makarius Efficient scanning of keywords and tokens. */ package isabelle import scala.annotation.tailrec import scala.collection.IndexedSeq import scala.util.matching.Regex import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader, CharSequenceReader, PagedSeq} import scala.util.parsing.combinator.RegexParsers import java.io.{File => JFile, BufferedInputStream, FileInputStream, InputStream} import java.net.URL object Scan { /** context of partial line-oriented scans **/ abstract class Line_Context case object Finished extends Line_Context case class Quoted(quote: String) extends Line_Context case object Verbatim extends Line_Context case class Cartouche(depth: Int) extends Line_Context case class Comment_Prefix(symbol: Symbol.Symbol) extends Line_Context case class Cartouche_Comment(depth: Int) extends Line_Context case class Comment(depth: Int) extends Line_Context /** parser combinators **/ object Parsers extends Parsers trait Parsers extends RegexParsers { override val whiteSpace: Regex = "".r /* optional termination */ def opt_term[T](p: => Parser[T]): Parser[Option[T]] = p ^^ (x => Some(x)) | """\z""".r ^^ (_ => None) /* repeated symbols */ def repeated(pred: Symbol.Symbol => Boolean, min_count: Int, max_count: Int): Parser[String] = new Parser[String] { def apply(in: Input) = { val start = in.offset val end = in.source.length val matcher = new Symbol.Matcher(in.source) var i = start var count = 0 var finished = false while (!finished && i < end && count < max_count) { val n = matcher(i, end) val sym = in.source.subSequence(i, i + n).toString if (pred(sym)) { i += n; count += 1 } else finished = true } if (count < min_count) Failure("bad input", in) else Success(in.source.subSequence(start, i).toString, in.drop(i - start)) } }.named("repeated") def one(pred: Symbol.Symbol => Boolean): Parser[String] = repeated(pred, 1, 1) def maybe(pred: Symbol.Symbol => Boolean): Parser[String] = repeated(pred, 0, 1) def many(pred: Symbol.Symbol => Boolean): Parser[String] = repeated(pred, 0, Integer.MAX_VALUE) def many1(pred: Symbol.Symbol => Boolean): Parser[String] = repeated(pred, 1, Integer.MAX_VALUE) /* character */ def character(pred: Char => Boolean): Symbol.Symbol => Boolean = (s: Symbol. Symbol) => s.length == 1 && pred(s.charAt(0)) /* quoted strings */ private def quoted_body(quote: Symbol.Symbol): Parser[String] = { rep(many1(sym => sym != quote && sym != "\\") | "\\" + quote | "\\\\" | ("""\\\d\d\d""".r ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ^^ (_.mkString) } def quoted(quote: Symbol.Symbol): Parser[String] = { quote ~ quoted_body(quote) ~ quote ^^ { case x ~ y ~ z => x + y + z } }.named("quoted") def quoted_content(quote: Symbol.Symbol, source: String): String = { require(parseAll(quoted(quote), source).successful, "no quoted text") val body = source.substring(1, source.length - 1) if (body.exists(_ == '\\')) { val content = rep(many1(sym => sym != quote && sym != "\\") | "\\" ~> (quote | "\\" | """\d\d\d""".r ^^ { case x => x.toInt.toChar.toString })) parseAll(content ^^ (_.mkString), body).get } else body } def quoted_line(quote: Symbol.Symbol, ctxt: Line_Context): Parser[(String, Line_Context)] = { ctxt match { case Finished => quote ~ quoted_body(quote) ~ opt_term(quote) ^^ { case x ~ y ~ Some(z) => (x + y + z, Finished) case x ~ y ~ None => (x + y, Quoted(quote)) } case Quoted(q) if q == quote => quoted_body(quote) ~ opt_term(quote) ^^ { case x ~ Some(y) => (x + y, Finished) case x ~ None => (x, ctxt) } case _ => failure("") } }.named("quoted_line") def recover_quoted(quote: Symbol.Symbol): Parser[String] = quote ~ quoted_body(quote) ^^ { case x ~ y => x + y } /* verbatim text */ private def verbatim_body: Parser[String] = rep(many1(sym => sym != "*") | """\*(?!\})""".r) ^^ (_.mkString) def verbatim: Parser[String] = { "{*" ~ verbatim_body ~ "*}" ^^ { case x ~ y ~ z => x + y + z } }.named("verbatim") def verbatim_content(source: String): String = { require(parseAll(verbatim, source).successful, "no verbatim text") source.substring(2, source.length - 2) } def verbatim_line(ctxt: Line_Context): Parser[(String, Line_Context)] = { ctxt match { case Finished => "{*" ~ verbatim_body ~ opt_term("*}") ^^ { case x ~ y ~ Some(z) => (x + y + z, Finished) case x ~ y ~ None => (x + y, Verbatim) } case Verbatim => verbatim_body ~ opt_term("*}") ^^ { case x ~ Some(y) => (x + y, Finished) case x ~ None => (x, Verbatim) } case _ => failure("") } }.named("verbatim_line") val recover_verbatim: Parser[String] = "{*" ~ verbatim_body ^^ { case x ~ y => x + y } /* nested text cartouches */ def cartouche_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)] { require(depth >= 0, "bad cartouche depth") def apply(in: Input) = { val start = in.offset val end = in.source.length val matcher = new Symbol.Matcher(in.source) var i = start var d = depth var finished = false while (!finished && i < end) { val n = matcher(i, end) val sym = in.source.subSequence(i, i + n).toString if (Symbol.is_open(sym)) { i += n; d += 1 } else if (Symbol.is_close(sym) && d > 0) { i += n; d -= 1; if (d == 0) finished = true } else if (d > 0) i += n else finished = true } if (i == start) Failure("bad input", in) else Success((in.source.subSequence(start, i).toString, d), in.drop(i - start)) } }.named("cartouche_depth") def cartouche: Parser[String] = cartouche_depth(0) ^? { case (x, d) if d == 0 => x } def cartouche_line(ctxt: Line_Context): Parser[(String, Line_Context)] = { def cartouche_context(d: Int): Line_Context = if (d == 0) Finished else Cartouche(d) ctxt match { case Finished => cartouche_depth(0) ^^ { case (c, d) => (c, cartouche_context(d)) } case Cartouche(depth) => cartouche_depth(depth) ^^ { case (c, d) => (c, cartouche_context(d)) } case _ => failure("") } } val recover_cartouche: Parser[String] = cartouche_depth(0) ^^ (_._1) def cartouche_content(source: String): String = { def err(): Nothing = error("Malformed text cartouche: " + quote(source)) val source1 = Library.try_unprefix(Symbol.open_decoded, source) orElse Library.try_unprefix(Symbol.open, source) getOrElse err() Library.try_unsuffix(Symbol.close_decoded, source1) orElse Library.try_unsuffix(Symbol.close, source1) getOrElse err() } /* nested comments */ private def comment_depth(depth: Int): Parser[(String, Int)] = new Parser[(String, Int)] { require(depth >= 0, "bad comment depth") val comment_text: Parser[List[String]] = rep1(many1(sym => sym != "*" && sym != "(") | """\*(?!\))|\((?!\*)""".r) def apply(in: Input) = { var rest = in def try_parse[A](p: Parser[A]): Boolean = { parse(p ^^^ (()), rest) match { case Success(_, next) => { rest = next; true } case _ => false } } var d = depth var finished = false while (!finished) { if (try_parse("(*")) d += 1 else if (d > 0 && try_parse("*)")) { d -= 1; if (d == 0) finished = true } else if (d == 0 || !try_parse(comment_text)) finished = true } if (in.offset < rest.offset) Success((in.source.subSequence(in.offset, rest.offset).toString, d), rest) else Failure("comment expected", in) } }.named("comment_depth") def comment: Parser[String] = comment_depth(0) ^? { case (x, d) if d == 0 => x } def comment_line(ctxt: Line_Context): Parser[(String, Line_Context)] = { val depth = ctxt match { case Finished => 0 case Comment(d) => d case _ => -1 } if (depth >= 0) comment_depth(depth) ^^ { case (x, 0) => (x, Finished) case (x, d) => (x, Comment(d)) } else failure("") } val recover_comment: Parser[String] = comment_depth(0) ^^ (_._1) def comment_content(source: String): String = { require(parseAll(comment, source).successful, "no comment") source.substring(2, source.length - 2) } /* keyword */ def literal(lexicon: Lexicon): Parser[String] = new Parser[String] { def apply(in: Input) = { val result = lexicon.scan(in) if (result.isEmpty) Failure("keyword expected", in) else Success(result, in.drop(result.length)) } }.named("keyword") } /** Lexicon -- position tree **/ object Lexicon { /* representation */ private sealed case class Tree(branches: Map[Char, (String, Tree)]) private val empty_tree = Tree(Map()) val empty: Lexicon = new Lexicon(empty_tree) def apply(elems: String*): Lexicon = empty ++ elems } final class Lexicon private(rep: Lexicon.Tree) { /* auxiliary operations */ private def dest(tree: Lexicon.Tree, result: List[String]): List[String] = tree.branches.toList.foldLeft(result) { case (res, (_, (s, tr))) => if (s.isEmpty) dest(tr, res) else dest(tr, s :: res) } private def lookup(str: CharSequence): Option[(Boolean, Lexicon.Tree)] = { val len = str.length @tailrec def look(tree: Lexicon.Tree, tip: Boolean, i: Int): Option[(Boolean, Lexicon.Tree)] = { if (i < len) { tree.branches.get(str.charAt(i)) match { case Some((s, tr)) => look(tr, s.nonEmpty, i + 1) case None => None } } else Some(tip, tree) } look(rep, false, 0) } def completions(str: CharSequence): List[String] = lookup(str) match { case Some((true, tree)) => dest(tree, List(str.toString)) case Some((false, tree)) => dest(tree, Nil) case None => Nil } /* pseudo Set methods */ def raw_iterator: Iterator[String] = dest(rep, Nil).iterator def iterator: Iterator[String] = dest(rep, Nil).sorted.iterator override def toString: String = iterator.mkString("Lexicon(", ", ", ")") def is_empty: Boolean = rep.branches.isEmpty def contains(elem: String): Boolean = lookup(elem) match { case Some((tip, _)) => tip case _ => false } /* build lexicon */ def + (elem: String): Lexicon = if (contains(elem)) this else { val len = elem.length def extend(tree: Lexicon.Tree, i: Int): Lexicon.Tree = if (i < len) { val c = elem.charAt(i) val end = (i + 1 == len) tree.branches.get(c) match { case Some((s, tr)) => Lexicon.Tree(tree.branches + (c -> (if (end) elem else s, extend(tr, i + 1)))) case None => Lexicon.Tree(tree.branches + (c -> (if (end) elem else "", extend(Lexicon.empty_tree, i + 1)))) } } else tree new Lexicon(extend(rep, 0)) } - def ++ (elems: IterableOnce[String]): Lexicon = elems.foldLeft(this)(_ + _) + def ++ (elems: IterableOnce[String]): Lexicon = + elems.iterator.foldLeft(this)(_ + _) def ++ (other: Lexicon): Lexicon = if (this eq other) this else if (is_empty) other else this ++ other.raw_iterator def -- (remove: Iterable[String]): Lexicon = if (remove.exists(contains)) Lexicon.empty ++ iterator.filterNot(a => remove.exists(b => a == b)) else this /* scan */ def scan(in: Reader[Char]): String = { val source = in.source val offset = in.offset val len = source.length - offset @tailrec def scan_tree(tree: Lexicon.Tree, result: String, i: Int): String = { if (i < len) { tree.branches.get(source.charAt(offset + i)) match { case Some((s, tr)) => scan_tree(tr, if (s.isEmpty) result else s, i + 1) case None => result } } else result } scan_tree(rep, "", 0) } } /** read stream without decoding: efficient length operation **/ private class Restricted_Seq(seq: IndexedSeq[Char], start: Int, end: Int) extends CharSequence { def charAt(i: Int): Char = if (0 <= i && i < length) seq(start + i) else throw new IndexOutOfBoundsException def length: Int = end - start // avoid expensive seq.length def subSequence(i: Int, j: Int): CharSequence = if (0 <= i && i <= j && j <= length) new Restricted_Seq(seq, start + i, start + j) else throw new IndexOutOfBoundsException override def toString: String = { val buf = new StringBuilder(length) for (offset <- start until end) buf.append(seq(offset)) buf.toString } } abstract class Byte_Reader extends Reader[Char] with AutoCloseable private def make_byte_reader(stream: InputStream, stream_length: Int): Byte_Reader = { val buffered_stream = new BufferedInputStream(stream) val seq = new PagedSeq( (buf: Array[Char], offset: Int, length: Int) => { var i = 0 var c = 0 var eof = false while (!eof && i < length) { c = buffered_stream.read if (c == -1) eof = true else { buf(offset + i) = c.toChar; i += 1 } } if (i > 0) i else -1 }) val restricted_seq = new Restricted_Seq(seq, 0, stream_length) class Paged_Reader(override val offset: Int) extends Byte_Reader { override lazy val source: CharSequence = restricted_seq def first: Char = if (seq.isDefinedAt(offset)) seq(offset) else '\u001a' def rest: Paged_Reader = if (seq.isDefinedAt(offset)) new Paged_Reader(offset + 1) else this def pos: InputPosition = new OffsetPosition(source, offset) def atEnd: Boolean = !seq.isDefinedAt(offset) override def drop(n: Int): Paged_Reader = new Paged_Reader(offset + n) def close: Unit = buffered_stream.close } new Paged_Reader(0) } def byte_reader(file: JFile): Byte_Reader = make_byte_reader(new FileInputStream(file), file.length.toInt) def byte_reader(url: URL): Byte_Reader = { val connection = url.openConnection val stream = connection.getInputStream val stream_length = connection.getContentLength make_byte_reader(stream, stream_length) } def reader_is_utf8(reader: Reader[Char]): Boolean = reader.isInstanceOf[Byte_Reader] def reader_decode_utf8(is_utf8: Boolean, s: String): String = if (is_utf8) UTF8.decode_permissive(s) else s def reader_decode_utf8(reader: Reader[Char], s: String): String = reader_decode_utf8(reader_is_utf8(reader), s) /* plain text reader */ def char_reader(text: CharSequence): CharSequenceReader = new CharSequenceReader(text) } diff --git a/src/Pure/PIDE/command.scala b/src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala +++ b/src/Pure/PIDE/command.scala @@ -1,653 +1,658 @@ /* Title: Pure/PIDE/command.scala Author: Fabian Immler, TU Munich Author: Makarius Prover commands with accumulated results from execution. */ package isabelle import scala.collection.immutable.SortedMap object Command { /* blobs */ object Blob { def read_file(name: Document.Node.Name, src_path: Path): Blob = { val bytes = Bytes.read(name.path) val chunk = Symbol.Text_Chunk(bytes.text) Blob(name, src_path, Some((bytes.sha1_digest, chunk))) } } sealed case class Blob( name: Document.Node.Name, src_path: Path, content: Option[(SHA1.Digest, Symbol.Text_Chunk)]) { def read_file: Bytes = Bytes.read(name.path) def chunk_file: Symbol.Text_Chunk.File = Symbol.Text_Chunk.File(name.node) } object Blobs_Info { val none: Blobs_Info = Blobs_Info(Nil) def errors(msgs: List[String]): Blobs_Info = Blobs_Info(msgs.map(msg => Exn.Exn[Blob](ERROR(msg)))) } sealed case class Blobs_Info(blobs: List[Exn.Result[Blob]], index: Int = -1) /** accumulated results from prover **/ /* results */ object Results { type Entry = (Long, XML.Elem) val empty: Results = new Results(SortedMap.empty) - def make(args: IterableOnce[Results.Entry]): Results = args.foldLeft(empty)(_ + _) - def merge(args: IterableOnce[Results]): Results = args.foldLeft(empty)(_ ++ _) + def make(args: IterableOnce[Results.Entry]): Results = + args.iterator.foldLeft(empty)(_ + _) + def merge(args: IterableOnce[Results]): Results = + args.iterator.foldLeft(empty)(_ ++ _) } final class Results private(private val rep: SortedMap[Long, XML.Elem]) { def is_empty: Boolean = rep.isEmpty def defined(serial: Long): Boolean = rep.isDefinedAt(serial) def get(serial: Long): Option[XML.Elem] = rep.get(serial) def iterator: Iterator[Results.Entry] = rep.iterator def + (entry: Results.Entry): Results = if (defined(entry._1)) this else new Results(rep + entry) def ++ (other: Results): Results = if (this eq other) this else if (rep.isEmpty) other else other.iterator.foldLeft(this)(_ + _) override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Results => rep == other.rep case _ => false } override def toString: String = iterator.mkString("Results(", ", ", ")") } /* exports */ object Exports { type Entry = (Long, Export.Entry) val empty: Exports = new Exports(SortedMap.empty) - def merge(args: IterableOnce[Exports]): Exports = args.foldLeft(empty)(_ ++ _) + def merge(args: IterableOnce[Exports]): Exports = + args.iterator.foldLeft(empty)(_ ++ _) } final class Exports private(private val rep: SortedMap[Long, Export.Entry]) { def is_empty: Boolean = rep.isEmpty def iterator: Iterator[Exports.Entry] = rep.iterator def + (entry: Exports.Entry): Exports = if (rep.isDefinedAt(entry._1)) this else new Exports(rep + entry) def ++ (other: Exports): Exports = if (this eq other) this else if (rep.isEmpty) other else other.iterator.foldLeft(this)(_ + _) override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Exports => rep == other.rep case _ => false } override def toString: String = iterator.mkString("Exports(", ", ", ")") } /* markups */ object Markup_Index { val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default) def blob(blob: Blob): Markup_Index = Markup_Index(false, blob.chunk_file) } sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name) object Markups { type Entry = (Markup_Index, Markup_Tree) val empty: Markups = new Markups(Map.empty) def init(markup: Markup_Tree): Markups = new Markups(Map(Markup_Index.markup -> markup)) - def make(args: IterableOnce[Entry]): Markups = args.foldLeft(empty)(_ + _) - def merge(args: IterableOnce[Markups]): Markups = args.foldLeft(empty)(_ ++ _) + def make(args: IterableOnce[Entry]): Markups = + args.iterator.foldLeft(empty)(_ + _) + def merge(args: IterableOnce[Markups]): Markups = + args.iterator.foldLeft(empty)(_ ++ _) } final class Markups private(private val rep: Map[Markup_Index, Markup_Tree]) { def is_empty: Boolean = rep.isEmpty def apply(index: Markup_Index): Markup_Tree = rep.getOrElse(index, Markup_Tree.empty) def add(index: Markup_Index, markup: Text.Markup): Markups = new Markups(rep + (index -> (this(index) + markup))) def + (entry: Markups.Entry): Markups = { val (index, tree) = entry new Markups(rep + (index -> (this(index).merge(tree, Text.Range.full, Markup.Elements.full)))) } def ++ (other: Markups): Markups = if (this eq other) this else if (rep.isEmpty) other else other.rep.iterator.foldLeft(this)(_ + _) def redirection_iterator: Iterator[Document_ID.Generic] = for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator) yield id def redirect(other_id: Document_ID.Generic): Markups = { val rep1 = (for { (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator if other_id == id } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap if (rep1.isEmpty) Markups.empty else new Markups(rep1) } override def hashCode: Int = rep.hashCode override def equals(that: Any): Boolean = that match { case other: Markups => rep == other.rep case _ => false } override def toString: String = rep.iterator.mkString("Markups(", ", ", ")") } /* state */ object State { def get_result(states: List[State], serial: Long): Option[XML.Elem] = states.find(st => st.results.defined(serial)).map(st => st.results.get(serial).get) def get_result_proper(states: List[State], props: Properties.T): Option[Results.Entry] = for { serial <- Markup.Serial.unapply(props) elem <- get_result(states, serial) if elem.body.nonEmpty } yield serial -> elem def merge_results(states: List[State]): Results = Results.merge(states.map(_.results)) def merge_exports(states: List[State]): Exports = Exports.merge(states.map(_.exports)) def merge_markups(states: List[State]): Markups = Markups.merge(states.map(_.markups)) def merge_markup(states: List[State], index: Markup_Index, range: Text.Range, elements: Markup.Elements): Markup_Tree = Markup_Tree.merge(states.map(_.markup(index)), range, elements) def merge(command: Command, states: List[State]): State = State(command, states.flatMap(_.status), merge_results(states), merge_exports(states), merge_markups(states)) } sealed case class State( command: Command, status: List[Markup] = Nil, results: Results = Results.empty, exports: Exports = Exports.empty, markups: Markups = Markups.empty) { def initialized: Boolean = status.exists(markup => markup.name == Markup.INITIALIZED) def consolidating: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATING) def consolidated: Boolean = status.exists(markup => markup.name == Markup.CONSOLIDATED) lazy val maybe_consolidated: Boolean = { var touched = false var forks = 0 var runs = 0 for (markup <- status) { markup.name match { case Markup.FORKED => touched = true; forks += 1 case Markup.JOINED => forks -= 1 case Markup.RUNNING => touched = true; runs += 1 case Markup.FINISHED => runs -= 1 case _ => } } touched && forks == 0 && runs == 0 } lazy val document_status: Document_Status.Command_Status = { val warnings = if (results.iterator.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2))) List(Markup(Markup.WARNING, Nil)) else Nil val errors = if (results.iterator.exists(p => Protocol.is_error(p._2))) List(Markup(Markup.ERROR, Nil)) else Nil Document_Status.Command_Status.make((warnings ::: errors ::: status).iterator) } def markup(index: Markup_Index): Markup_Tree = markups(index) def redirect(other_command: Command): Option[State] = { val markups1 = markups.redirect(other_command.id) if (markups1.is_empty) None else Some(new State(other_command, markups = markups1)) } private def add_status(st: Markup): State = copy(status = st :: status) private def add_result(entry: Results.Entry): State = copy(results = results + entry) def add_export(entry: Exports.Entry): Option[State] = if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry)) else None private def add_markup( status: Boolean, chunk_name: Symbol.Text_Chunk.Name, m: Text.Markup): State = { val markups1 = if (status || Document_Status.Command_Status.liberal_elements(m.info.name)) markups.add(Markup_Index(true, chunk_name), m) else markups copy(markups = markups1.add(Markup_Index(false, chunk_name), m)) } def accumulate( self_id: Document_ID.Generic => Boolean, other_id: (Document.Node.Name, Document_ID.Generic) => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)], message: XML.Elem, cache: XML.Cache): State = message match { case XML.Elem(Markup(Markup.STATUS, _), msgs) => if (command.span.is_theory) this else { msgs.foldLeft(this) { case (state, msg) => msg match { case elem @ XML.Elem(markup, Nil) => state. add_status(markup). add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.core_range, elem)) case _ => Output.warning("Ignored status message: " + msg) state } } } case XML.Elem(Markup(Markup.REPORT, atts0), msgs) => msgs.foldLeft(this) { case (state, msg) => def bad(): Unit = Output.warning("Ignored report message: " + msg) msg match { case XML.Elem(Markup(name, atts), args) => command.reported_position(atts) orElse command.reported_position(atts0) match { case Some((id, chunk_name, target_range)) => val target = if (self_id(id) && command.chunks.isDefinedAt(chunk_name)) Some((chunk_name, command.chunks(chunk_name))) else if (chunk_name == Symbol.Text_Chunk.Default) other_id(command.node_name, id) else None (target, target_range) match { case (Some((target_name, target_chunk)), Some(symbol_range)) if !symbol_range.is_singularity => target_chunk.incorporate(symbol_range) match { case Some(range) => val props = atts.filterNot(Markup.position_property) val elem = cache.elem(XML.Elem(Markup(name, props), args)) state.add_markup(false, target_name, Text.Info(range, elem)) case None => bad(); state } case _ => // silently ignore excessive reports state } case _ => bad(); state } case _ => bad(); state } } case XML.Elem(Markup(name, props), body) => props match { case Markup.Serial(i) => val markup_message = cache.elem(XML.Elem(Markup(Markup.message(name), props), body)) val message_markup = cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL)))) var st = add_result(i -> markup_message) if (Protocol.is_inlined(message)) { for { (chunk_name, chunk) <- command.chunks.iterator range <- command.message_positions(self_id, chunk_name, chunk, message) } st = st.add_markup(false, chunk_name, Text.Info(range, message_markup)) } st case _ => Output.warning("Ignored message without serial number: " + message) this } } } /** static content **/ /* make commands */ def apply( id: Document_ID.Command, node_name: Document.Node.Name, blobs_info: Blobs_Info, span: Command_Span.Span): Command = { val (source, span1) = span.compact_source new Command(id, node_name, blobs_info, span1, source, Results.empty, Markups.empty) } val empty: Command = Command(Document_ID.none, Document.Node.Name.empty, Blobs_Info.none, Command_Span.empty) def unparsed( source: String, theory: Boolean = false, id: Document_ID.Command = Document_ID.none, node_name: Document.Node.Name = Document.Node.Name.empty, blobs_info: Blobs_Info = Blobs_Info.none, results: Results = Results.empty, markups: Markups = Markups.empty): Command = { val (source1, span1) = Command_Span.unparsed(source, theory).compact_source new Command(id, node_name, blobs_info, span1, source1, results, markups) } def text(source: String): Command = unparsed(source) def rich_text(id: Document_ID.Command, results: Results, body: XML.Body): Command = unparsed(XML.content(body), id = id, results = results, markups = Markups.init(Markup_Tree.from_XML(body))) /* edits and perspective */ type Edit = (Option[Command], Option[Command]) object Perspective { val empty: Perspective = Perspective(Nil) } sealed case class Perspective(commands: List[Command]) // visible commands in canonical order { def is_empty: Boolean = commands.isEmpty def same(that: Perspective): Boolean = { val cmds1 = this.commands val cmds2 = that.commands require(!cmds1.exists(_.is_undefined), "cmds1 not defined") require(!cmds2.exists(_.is_undefined), "cmds2 not defined") cmds1.length == cmds2.length && (cmds1.iterator zip cmds2.iterator).forall({ case (c1, c2) => c1.id == c2.id }) } } /* blobs: inlined errors and auxiliary files */ def blobs_info( resources: Resources, syntax: Outer_Syntax, get_blob: Document.Node.Name => Option[Document.Blob], can_import: Document.Node.Name => Boolean, node_name: Document.Node.Name, span: Command_Span.Span): Blobs_Info = { span.name match { // inlined errors case Thy_Header.THEORY => val reader = span.content_reader val header = resources.check_thy(node_name, span.content_reader) val imports_pos = header.imports_pos val raw_imports = try { val read_imports = Thy_Header.read(node_name, reader).imports.map(_._1) if (imports_pos.length == read_imports.length) read_imports else error("") } catch { case _: Throwable => List.fill(header.imports.length)("") } val errors = for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) } yield { val completion = if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil "Bad theory import " + Markup.Path(import_name.node).markup(quote(import_name.toString)) + Position.here(pos) + Completion.report_theories(pos, completion) } Blobs_Info.errors(errors) // auxiliary files case _ => val loaded_files = span.loaded_files(syntax) val blobs = loaded_files.files.map(file => (Exn.capture { val src_path = Path.explode(file) val name = Document.Node.Name(resources.append(node_name, src_path)) val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk)) Blob(name, src_path, content) }).user_error) Blobs_Info(blobs, index = loaded_files.index) } } def build_blobs_info( syntax: Outer_Syntax, node_name: Document.Node.Name, load_commands: List[Command_Span.Span]): Blobs_Info = { val blobs = for { span <- load_commands file <- span.loaded_files(syntax).files } yield { (Exn.capture { val dir = node_name.master_dir_path val src_path = Path.explode(file) val name = Document.Node.Name((dir + src_path).expand.implode_symbolic) Blob.read_file(name, src_path) }).user_error } Blobs_Info(blobs) } } final class Command private( val id: Document_ID.Command, val node_name: Document.Node.Name, val blobs_info: Command.Blobs_Info, val span: Command_Span.Span, val source: String, val init_results: Command.Results, val init_markups: Command.Markups) { override def toString: String = id + "/" + span.kind.toString /* classification */ def is_proper: Boolean = span.kind.isInstanceOf[Command_Span.Command_Span] def is_ignored: Boolean = span.kind == Command_Span.Ignored_Span def is_undefined: Boolean = id == Document_ID.none val is_unparsed: Boolean = span.content.exists(_.is_unparsed) val is_unfinished: Boolean = span.content.exists(_.is_unfinished) def potentially_initialized: Boolean = span.name == Thy_Header.THEORY /* blobs */ def blobs: List[Exn.Result[Command.Blob]] = blobs_info.blobs def blobs_index: Int = blobs_info.index def blobs_ok: Boolean = blobs.forall({ case Exn.Res(_) => true case _ => false }) def blobs_names: List[Document.Node.Name] = for (Exn.Res(blob) <- blobs) yield blob.name def blobs_undefined: List[Document.Node.Name] = for (Exn.Res(blob) <- blobs if blob.content.isEmpty) yield blob.name def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] = for (Exn.Res(blob) <- blobs; (digest, _) <- blob.content) yield (blob.name, digest) def blobs_changed(doc_blobs: Document.Blobs): Boolean = blobs.exists({ case Exn.Res(blob) => doc_blobs.changed(blob.name) case _ => false }) /* source chunks */ val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(source) val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] = ((Symbol.Text_Chunk.Default -> chunk) :: (for (Exn.Res(blob) <- blobs; (_, file) <- blob.content) yield blob.chunk_file -> file)).toMap def length: Int = source.length def range: Text.Range = chunk.range val core_range: Text.Range = Text.Range(0, span.content.reverse.iterator.takeWhile(_.is_ignored).foldLeft(length)(_ - _.source.length)) def source(range: Text.Range): String = range.substring(source) /* theory parents */ def theory_parents(resources: Resources): List[Document.Node.Name] = if (span.name == Thy_Header.THEORY) { try { val header = Thy_Header.read(node_name, span.content_reader) for ((s, _) <- header.imports) yield { try { resources.import_name(node_name, s) } catch { case ERROR(_) => Document.Node.Name.empty } } } catch { case ERROR(_) => Nil } } else Nil /* reported positions */ def reported_position(pos: Position.T) : Option[(Document_ID.Generic, Symbol.Text_Chunk.Name, Option[Symbol.Range])] = { pos match { case Position.Id(id) => val chunk_name = pos match { case Position.File(name) if name != node_name.node => Symbol.Text_Chunk.File(name) case _ => Symbol.Text_Chunk.Default } Some((id, chunk_name, Position.Range.unapply(pos))) case _ => None } } def message_positions( self_id: Document_ID.Generic => Boolean, chunk_name: Symbol.Text_Chunk.Name, chunk: Symbol.Text_Chunk, message: XML.Elem): Set[Text.Range] = { def elem(props: Properties.T, set: Set[Text.Range]): Set[Text.Range] = reported_position(props) match { case Some((id, name, reported_range)) if self_id(id) && name == chunk_name => val opt_range = reported_range orElse { if (name == Symbol.Text_Chunk.Default) Position.Range.unapply(span.position) else None } opt_range match { case Some(symbol_range) => chunk.incorporate(symbol_range) match { case Some(range) => set + range case _ => set } case None => set } case _ => set } def tree(set: Set[Text.Range], t: XML.Tree): Set[Text.Range] = t match { case XML.Wrapped_Elem(Markup(name, props), _, body) => body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree) case XML.Elem(Markup(name, props), body) => body.foldLeft(if (Rendering.position_elements(name)) elem(props, set) else set)(tree) case XML.Text(_) => set } val set = tree(Set.empty, message) if (set.isEmpty) elem(message.markup.properties, set) else set } /* accumulated results */ val init_state: Command.State = Command.State(this, results = init_results, markups = init_markups) val empty_state: Command.State = Command.State(this) } diff --git a/src/Pure/library.scala b/src/Pure/library.scala --- a/src/Pure/library.scala +++ b/src/Pure/library.scala @@ -1,299 +1,303 @@ /* Title: Pure/library.scala Author: Makarius Basic library. */ package isabelle import scala.annotation.tailrec import scala.collection.mutable import scala.util.matching.Regex object Library { /* resource management */ def using[A <: AutoCloseable, B](a: A)(f: A => B): B = { try { f(a) } finally { if (a != null) a.close() } } /* integers */ private val small_int = 10000 private lazy val small_int_table = { val array = new Array[String](small_int) for (i <- 0 until small_int) array(i) = i.toString array } def is_small_int(s: String): Boolean = { val len = s.length 1 <= len && len <= 4 && s.forall(c => '0' <= c && c <= '9') && (len == 1 || s(0) != '0') } def signed_string_of_long(i: Long): String = if (0 <= i && i < small_int) small_int_table(i.toInt) else i.toString def signed_string_of_int(i: Int): String = if (0 <= i && i < small_int) small_int_table(i) else i.toString /* separated chunks */ def separate[A](s: A, list: List[A]): List[A] = { val result = new mutable.ListBuffer[A] var first = true for (x <- list) { if (first) { first = false result += x } else { result += s result += x } } result.toList } def separated_chunks(sep: Char => Boolean, source: CharSequence): Iterator[CharSequence] = new Iterator[CharSequence] { private val end = source.length private def next_chunk(i: Int): Option[(CharSequence, Int)] = { if (i < end) { var j = i; do j += 1 while (j < end && !sep(source.charAt(j))) Some((source.subSequence(i + 1, j), j)) } else None } private var state: Option[(CharSequence, Int)] = if (end == 0) None else next_chunk(-1) def hasNext: Boolean = state.isDefined def next(): CharSequence = state match { case Some((s, i)) => state = next_chunk(i); s case None => Iterator.empty.next() } } def space_explode(sep: Char, str: String): List[String] = separated_chunks(_ == sep, str).map(_.toString).toList /* lines */ - def terminate_lines(lines: IterableOnce[String]): String = lines.mkString("", "\n", "\n") + def terminate_lines(lines: IterableOnce[String]): String = + lines.iterator.mkString("", "\n", "\n") - def cat_lines(lines: IterableOnce[String]): String = lines.mkString("\n") + def cat_lines(lines: IterableOnce[String]): String = + lines.iterator.mkString("\n") def split_lines(str: String): List[String] = space_explode('\n', str) def prefix_lines(prfx: String, str: String): String = if (str == "") str else cat_lines(split_lines(str).map(prfx + _)) def first_line(source: CharSequence): String = { val lines = separated_chunks(_ == '\n', source) if (lines.hasNext) lines.next().toString else "" } def trim_line(s: String): String = if (s.endsWith("\r\n")) s.substring(0, s.length - 2) else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1) else s def trim_split_lines(s: String): List[String] = split_lines(trim_line(s)).map(trim_line) def encode_lines(s: String): String = s.replace('\n', '\u000b') def decode_lines(s: String): String = s.replace('\u000b', '\n') /* strings */ - def cat_strings0(strs: IterableOnce[String]): String = strs.mkString("\u0000") + def cat_strings0(strs: IterableOnce[String]): String = + strs.iterator.mkString("\u0000") + def split_strings0(str: String): List[String] = space_explode('\u0000', str) def make_string(f: StringBuilder => Unit): String = { val s = new StringBuilder f(s) s.toString } def try_unprefix(prfx: String, s: String): Option[String] = if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None def try_unsuffix(sffx: String, s: String): Option[String] = if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None def perhaps_unprefix(prfx: String, s: String): String = try_unprefix(prfx, s) getOrElse s def perhaps_unsuffix(sffx: String, s: String): String = try_unsuffix(sffx, s) getOrElse s def isolate_substring(s: String): String = new String(s.toCharArray) def strip_ansi_color(s: String): String = s.replaceAll("\u001b\\[\\d+m", "") /* quote */ def single_quote(s: String): String = "'" + s + "'" def quote(s: String): String = "\"" + s + "\"" def try_unquote(s: String): Option[String] = if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1)) else None def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ") def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ") /* CharSequence */ class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence { require(0 <= start && start <= end && end <= text.length, "bad reverse range") def this(text: CharSequence) = this(text, 0, text.length) def length: Int = end - start def charAt(i: Int): Char = text.charAt(end - i - 1) def subSequence(i: Int, j: Int): CharSequence = if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i) else throw new IndexOutOfBoundsException override def toString: String = { val buf = new StringBuilder(length) for (i <- 0 until length) buf.append(charAt(i)) buf.toString } } class Line_Termination(text: CharSequence) extends CharSequence { def length: Int = text.length + 1 def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i) def subSequence(i: Int, j: Int): CharSequence = if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1)) else text.subSequence(i, j) override def toString: String = text.toString + "\n" } /* regular expressions */ def make_regex(s: String): Option[Regex] = try { Some(new Regex(s)) } catch { case ERROR(_) => None } def is_regex_meta(c: Char): Boolean = """()[]{}\^$|?*+.<>-=!""".contains(c) def escape_regex(s: String): String = if (s.exists(is_regex_meta)) { (for (c <- s.iterator) yield { if (is_regex_meta(c)) "\\" + c.toString else c.toString }).mkString } else s /* lists */ def take_prefix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) = (xs.takeWhile(pred), xs.dropWhile(pred)) def take_suffix[A](pred: A => Boolean, xs: List[A]): (List[A], List[A]) = { val rev_xs = xs.reverse (rev_xs.dropWhile(pred).reverse, rev_xs.takeWhile(pred).reverse) } def trim[A](pred: A => Boolean, xs: List[A]): List[A] = take_suffix(pred, take_prefix(pred, xs)._2)._1 def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x) def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs) def merge[A](xs: List[A], ys: List[A]): List[A] = if (xs.eq(ys)) xs else if (xs.isEmpty) ys else ys.foldRight(xs)(Library.insert(_)(_)) def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = { val result = new mutable.ListBuffer[A] xs.foreach(x => if (!result.exists(y => eq(x, y))) result += x) result.toList } def duplicates[A](lst: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] = { val result = new mutable.ListBuffer[A] @tailrec def dups(rest: List[A]): Unit = rest match { case Nil => case x :: xs => if (!result.exists(y => eq(x, y)) && xs.exists(y => eq(x, y))) result += x dups(xs) } dups(lst) result.toList } def replicate[A](n: Int, a: A): List[A] = if (n < 0) throw new IllegalArgumentException else if (n == 0) Nil else { val res = new mutable.ListBuffer[A] (1 to n).foreach(_ => res += a) res.toList } /* proper values */ def proper_string(s: String): Option[String] = if (s == null || s == "") None else Some(s) def proper_list[A](list: List[A]): Option[List[A]] = if (list == null || list.isEmpty) None else Some(list) /* reflection */ def is_subclass[A, B](a: Class[A], b: Class[B]): Boolean = { import scala.language.existentials @tailrec def subclass(c: Class[_]): Boolean = { c == b || { val d = c.getSuperclass d != null && subclass(d) } } subclass(a) } }