diff --git a/src/Pure/General/completion.scala b/src/Pure/General/completion.scala --- a/src/Pure/General/completion.scala +++ b/src/Pure/General/completion.scala @@ -1,516 +1,516 @@ /* Title: Pure/General/completion.scala Author: Makarius Semantic completion within the formal context (reported names). Syntactic completion of keywords and symbols, with abbreviations (based on language context). */ package isabelle import scala.collection.immutable.SortedMap import scala.util.parsing.combinator.RegexParsers import scala.util.matching.Regex import scala.math.Ordering object Completion { /** completion result **/ sealed case class Item( range: Text.Range, original: String, name: String, description: List[String], replacement: String, move: Int, immediate: Boolean) object Result { def empty(range: Text.Range): Result = Result(range, "", false, Nil) def merge(history: History, results: Option[Result]*): Option[Result] = ((None: Option[Result]) /: results)({ case (result1, None) => result1 case (None, result2) => result2 case (result1 @ Some(res1), Some(res2)) => if (res1.range != res2.range || res1.original != res2.original) result1 else { val items = (res1.items ::: res2.items).sorted(history.ordering) Some(Result(res1.range, res1.original, false, items)) } }) } sealed case class Result( range: Text.Range, original: String, unique: Boolean, items: List[Item]) /** persistent history **/ private val COMPLETION_HISTORY = Path.explode("$ISABELLE_HOME_USER/etc/completion_history") object History { val empty: History = new History() def load(): History = { def ignore_error(msg: String): Unit = Output.warning("Ignoring bad content of file " + COMPLETION_HISTORY + (if (msg == "") "" else "\n" + msg)) val content = if (COMPLETION_HISTORY.is_file) { try { import XML.Decode._ list(pair(string, int))(Symbol.decode_yxml(File.read(COMPLETION_HISTORY))) } catch { case ERROR(msg) => ignore_error(msg); Nil case _: XML.Error => ignore_error(""); Nil } } else Nil (empty /: content)(_ + _) } } final class History private(rep: SortedMap[String, Int] = SortedMap.empty) { override def toString: String = rep.mkString("Completion.History(", ",", ")") def frequency(name: String): Int = default_frequency(Symbol.encode(name)) getOrElse rep.getOrElse(name, 0) def + (entry: (String, Int)): History = { val (name, freq) = entry if (name == "") this else new History(rep + (name -> (frequency(name) + freq))) } def ordering: Ordering[Item] = new Ordering[Item] { def compare(item1: Item, item2: Item): Int = frequency(item2.name) compare frequency(item1.name) } def save() { Isabelle_System.make_directory(COMPLETION_HISTORY.dir) File.write_backup(COMPLETION_HISTORY, { import XML.Encode._ Symbol.encode_yxml(list(pair(string, int))(rep.toList)) }) } } class History_Variable { private var history = History.empty def value: History = synchronized { history } def load() { val h = History.load() synchronized { history = h } } def update(item: Item, freq: Int = 1): Unit = synchronized { history = history + (item.name -> freq) } } /** semantic completion **/ def clean_name(s: String): Option[String] = if (s == "" || s == "_") None else Some(s.reverseIterator.dropWhile(_ == '_').toList.reverse.mkString) def completed(input: String): String => Boolean = clean_name(input) match { case None => (name: String) => false case Some(prefix) => (name: String) => name.startsWith(prefix) } def report_no_completion(pos: Position.T): String = YXML.string_of_tree(Semantic.Info(pos, No_Completion)) def report_names(pos: Position.T, names: List[(String, (String, String))], total: Int = 0): String = if (names.isEmpty) "" else YXML.string_of_tree(Semantic.Info(pos, Names(if (total > 0) total else names.length, names))) def report_theories(pos: Position.T, thys: List[String], total: Int = 0): String = - report_names(pos, thys.map(name => (name, ("theory", name))), total) + report_names(pos, thys.map(name => (name, (Markup.THEORY, name))), total) object Semantic { object Info { def apply(pos: Position.T, semantic: Semantic): XML.Elem = { val elem = semantic match { case No_Completion => XML.Elem(Markup(Markup.NO_COMPLETION, pos), Nil) case Names(total, names) => XML.Elem(Markup(Markup.COMPLETION, pos), { import XML.Encode._ pair(int, list(pair(string, pair(string, string))))(total, names) }) } XML.Elem(Markup(Markup.REPORT, pos), List(elem)) } def unapply(info: Text.Markup): Option[Text.Info[Semantic]] = info.info match { case XML.Elem(Markup(Markup.COMPLETION, _), body) => try { val (total, names) = { import XML.Decode._ pair(int, list(pair(string, pair(string, string))))(body) } Some(Text.Info(info.range, Names(total, names))) } catch { case _: XML.Error => None } case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) => Some(Text.Info(info.range, No_Completion)) case _ => None } } } sealed abstract class Semantic case object No_Completion extends Semantic case class Names(total: Int, names: List[(String, (String, String))]) extends Semantic { def complete( range: Text.Range, history: Completion.History, unicode: Boolean, original: String): Option[Completion.Result] = { def decode(s: String): String = if (unicode) Symbol.decode(s) else s val items = for { (xname, (kind, name)) <- names xname1 = decode(xname) if xname1 != original (full_name, descr_name) = if (kind == "") (name, quote(decode(name))) else (Long_Name.qualify(kind, name), Word.implode(Word.explode('_', kind)) + (if (xname == name) "" else " " + quote(decode(name)))) } yield { val description = List(xname1, "(" + descr_name + ")") val replacement = List(original, xname1).map(Token.explode(Keyword.Keywords.empty, _)) match { case List(List(tok), _) if tok.kind == Token.Kind.CARTOUCHE => Symbol.cartouche_decoded(xname1) case List(_, List(tok)) if tok.is_name => xname1 case _ => quote(xname1) } Item(range, original, full_name, description, replacement, 0, true) } if (items.isEmpty) None else Some(Result(range, original, names.length == 1, items.sorted(history.ordering))) } } /** syntactic completion **/ /* language context */ object Language_Context { val outer = Language_Context("", true, false) val inner = Language_Context(Markup.Language.UNKNOWN, true, false) val ML_outer = Language_Context(Markup.Language.ML, false, true) val ML_inner = Language_Context(Markup.Language.ML, true, false) val SML_outer = Language_Context(Markup.Language.SML, false, false) } sealed case class Language_Context(language: String, symbols: Boolean, antiquotes: Boolean) { def is_outer: Boolean = language == "" } /* make */ val empty: Completion = new Completion() def make(keywords: List[String], abbrevs: List[(String, String)]): Completion = empty.add_symbols.add_keywords(keywords).add_abbrevs( Completion.symbol_abbrevs ::: Completion.default_abbrevs ::: abbrevs) /* word parsers */ object Word_Parsers extends RegexParsers { override val whiteSpace = "".r private val symboloid_regex: Regex = """\\([A-Za-z0-9_']+|<\^?[A-Za-z0-9_']+>?)""".r def is_symboloid(s: CharSequence): Boolean = symboloid_regex.pattern.matcher(s).matches private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r private def reverse_escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r private val word_regex = "[a-zA-Z0-9_'.]+".r private def word2: Parser[String] = "[a-zA-Z0-9_'.]{2,}".r private def underscores: Parser[String] = "_*".r def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.' def read_symbol(in: CharSequence): Option[String] = { val reverse_in = new Library.Reverse(in) parse(reverse_symbol ^^ (_.reverse), reverse_in) match { case Success(result, _) => Some(result) case _ => None } } def read_word(in: CharSequence): Option[(String, String)] = { val reverse_in = new Library.Reverse(in) val parser = (reverse_symbol | reverse_symb | reverse_escape) ^^ (x => (x.reverse, "")) | underscores ~ word2 ~ opt("?") ^^ { case x ~ y ~ z => (z.getOrElse("") + y.reverse, x) } parse(parser, reverse_in) match { case Success(result, _) => Some(result) case _ => None } } } /* templates */ val caret_indicator = '\u0007' def split_template(s: String): (String, String) = space_explode(caret_indicator, s) match { case List(s1, s2) => (s1, s2) case _ => (s, "") } /* abbreviations */ private def symbol_abbrevs: Thy_Header.Abbrevs = for ((sym, abbr) <- Symbol.abbrevs.toList) yield (abbr, sym) private val antiquote = "@{" private val default_abbrevs = List("@{" -> "@{\u0007}", "`" -> "\\", "`" -> "\\", "`" -> "\\\u0007\\", "\"" -> "\\", "\"" -> "\\", "\"" -> "\\\u0007\\") private def default_frequency(name: String): Option[Int] = default_abbrevs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2) } final class Completion private( keywords: Set[String] = Set.empty, words_lex: Scan.Lexicon = Scan.Lexicon.empty, words_map: Multi_Map[String, String] = Multi_Map.empty, abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty, abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty) { /* keywords */ private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name) private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords(name) private def is_keyword_template(name: String, template: Boolean): Boolean = is_keyword(name) && (words_map.getOrElse(name, name) != name) == template def add_keyword(keyword: String): Completion = new Completion(keywords + keyword, words_lex, words_map, abbrevs_lex, abbrevs_map) def add_keywords(names: List[String]): Completion = { val keywords1 = (keywords /: names) { case (ks, k) => if (ks(k)) ks else ks + k } if (keywords eq keywords1) this else new Completion(keywords1, words_lex, words_map, abbrevs_lex, abbrevs_map) } /* symbols and abbrevs */ def add_symbols: Completion = { val words = Symbol.names.toList.flatMap({ case (sym, (name, argument)) => val word = "\\" + name val seps = if (argument == Symbol.ARGUMENT_CARTOUCHE) List("") else if (argument == Symbol.ARGUMENT_SPACE_CARTOUCHE) List(" ") else Nil List(sym -> sym, word -> sym) ::: seps.map(sep => word -> (sym + sep + "\\\u0007\\")) }) new Completion( keywords, words_lex ++ words.map(_._1), words_map ++ words, abbrevs_lex, abbrevs_map) } def add_abbrevs(abbrevs: List[(String, String)]): Completion = (this /: abbrevs)(_.add_abbrev(_)) private def add_abbrev(abbrev: (String, String)): Completion = abbrev match { case ("", _) => this case (abbr, text) => val rev_abbr = abbr.reverse val is_word = Completion.Word_Parsers.is_word(abbr) val (words_lex1, words_map1) = if (!is_word) (words_lex, words_map) else if (text != "") (words_lex + abbr, words_map + abbrev) else (words_lex -- List(abbr), words_map - abbr) val (abbrevs_lex1, abbrevs_map1) = if (is_word) (abbrevs_lex, abbrevs_map) else if (text != "") (abbrevs_lex + rev_abbr, abbrevs_map + (rev_abbr -> abbrev)) else (abbrevs_lex -- List(rev_abbr), abbrevs_map - rev_abbr) new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1) } /* complete */ def complete( history: Completion.History, unicode: Boolean, explicit: Boolean, start: Text.Offset, text: CharSequence, caret: Int, language_context: Completion.Language_Context): Option[Completion.Result] = { val length = text.length val abbrevs_result = { val reverse_in = new Library.Reverse(text.subSequence(0, caret)) Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), reverse_in) match { case Scan.Parsers.Success(reverse_abbr, _) => val abbrevs = abbrevs_map.get_list(reverse_abbr) abbrevs match { case Nil => None case (abbr, _) :: _ => val ok = if (abbr == Completion.antiquote) language_context.antiquotes else language_context.symbols || Completion.default_abbrevs.exists(_._1 == abbr) if (ok) Some((abbr, abbrevs)) else None } case _ => None } } val words_result = if (abbrevs_result.isDefined) None else { val word_context = caret < length && Completion.Word_Parsers.is_word_char(text.charAt(caret)) val result = Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match { case Some(symbol) => Some((symbol, "")) case None => Completion.Word_Parsers.read_word(text.subSequence(0, caret)) } result.map( { case (word, underscores) => val complete_words = words_lex.completions(word) val full_word = word + underscores val completions = if (complete_words.contains(full_word) && is_keyword_template(full_word, false)) Nil else for { complete_word <- complete_words ok = if (is_keyword(complete_word)) !word_context && language_context.is_outer else language_context.symbols || Completion.Word_Parsers.is_symboloid(word) if ok completion <- words_map.get_list(complete_word) } yield (complete_word, completion) (full_word, completions) }) } (abbrevs_result orElse words_result) match { case Some((original, completions)) if completions.nonEmpty => val range = Text.Range(- original.length, 0) + caret + start val immediate = explicit || (!Completion.Word_Parsers.is_word(original) && !Completion.Word_Parsers.is_symboloid(original) && Character.codePointCount(original, 0, original.length) > 1) val unique = completions.length == 1 def decode1(s: String): String = if (unicode) Symbol.decode(s) else s def decode2(s: String): String = if (unicode) s else Symbol.decode(s) val items = for { (complete_word, name0) <- completions name1 = decode1(name0) name2 = decode2(name0) if name1 != original (s1, s2) = Completion.split_template(name1) move = - s2.length description = if (is_symbol(name0)) { if (name1 == name2) List(name1) else List(name1, "(symbol " + quote(name2) + ")") } else if (is_keyword_template(complete_word, true)) List(name1, "(template " + quote(complete_word) + ")") else if (move != 0) List(name1, "(template)") else if (is_keyword(complete_word)) List(name1, "(keyword)") else List(name1) } yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate) if (items.isEmpty) None else Some(Completion.Result(range, original, unique, items.sortBy(_.name).sorted(history.ordering))) case _ => None } } } 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,713 +1,714 @@ /* 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" object Entity { val Def = new Properties.Long("def") val Ref = new Properties.Long("ref") 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 } } /* 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" /* 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 Finished_Theory extends Name_Function("finished_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) }) def + (entry: Properties.Entry): Markup = Markup(name, Properties.put(properties, entry)) }