diff --git a/src/Pure/Admin/build_history.scala b/src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala +++ b/src/Pure/Admin/build_history.scala @@ -1,603 +1,611 @@ /* Title: Pure/Admin/build_history.scala Author: Makarius Build other history versions. */ package isabelle import java.io.{File => JFile} import java.time.format.DateTimeFormatter import java.util.Locale object Build_History { /* log files */ val engine = "build_history" val log_prefix = engine + "_" /* augment settings */ def augment_settings( other_isabelle: Other_Isabelle, threads: Int, arch_64: Boolean, heap: Int, max_heap: Option[Int], more_settings: List[String]): String = { val (ml_platform, ml_settings) = { val windows_32 = "x86-windows" val windows_64 = "x86_64-windows" val windows_64_32 = "x86_64_32-windows" val platform_32 = other_isabelle.getenv("ISABELLE_PLATFORM32") val platform_64 = other_isabelle.getenv("ISABELLE_PLATFORM64") val platform_64_32 = platform_64.replace("x86_64-", "x86_64_32-") val polyml_home = try { Path.explode(other_isabelle.getenv("ML_HOME")).dir } catch { case ERROR(msg) => error("Bad ML_HOME: " + msg) } def ml_home(platform: String): Path = polyml_home + Path.explode(platform) def err(platform: String): Nothing = error("Platform " + platform + " unavailable on this machine") def check_dir(platform: String): Boolean = platform != "" && ml_home(platform).is_dir val ml_platform = if (Platform.is_windows && arch_64) { if (check_dir(windows_64)) windows_64 else err(windows_64) } else if (Platform.is_windows && !arch_64) { if (check_dir(windows_64_32)) windows_64_32 else if (check_dir(windows_32)) windows_32 else platform_32 // x86-cygwin } else if (arch_64) { if (check_dir(platform_64)) platform_64 else err(platform_64) } else if (check_dir(platform_64_32)) platform_64_32 else platform_32 val ml_options = "--minheap " + heap + (if (max_heap.isDefined) " --maxheap " + max_heap.get else "") + " --gcthreads " + threads + (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "") (ml_platform, List( "ML_HOME=" + File.bash_path(ml_home(ml_platform)), "ML_PLATFORM=" + quote(ml_platform), "ML_OPTIONS=" + quote(ml_options))) } val thread_settings = List( "ISABELLE_JAVA_SYSTEM_OPTIONS=\"$ISABELLE_JAVA_SYSTEM_OPTIONS -Disabelle.threads=" + threads + "\"", "ISABELLE_BUILD_OPTIONS=\"threads=" + threads + "\"") val settings = List(ml_settings, thread_settings) ::: (if (more_settings.isEmpty) Nil else List(more_settings)) File.append(other_isabelle.etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_)))) ml_platform } /** build_history **/ private val default_user_home = Path.explode("$USER_HOME") private val default_rev = "tip" private val default_multicore = (1, 1) private val default_heap = 1500 private val default_isabelle_identifier = "build_history" def build_history( options: Options, root: Path, user_home: Path = default_user_home, progress: Progress = new Progress, rev: String = default_rev, afp_rev: Option[String] = None, afp_partition: Int = 0, isabelle_identifier: String = default_isabelle_identifier, ml_statistics_step: Int = 1, components_base: Path = Components.default_components_base, fresh: Boolean = false, hostname: String = "", multicore_base: Boolean = false, multicore_list: List[(Int, Int)] = List(default_multicore), arch_64: Boolean = false, heap: Int = default_heap, max_heap: Option[Int] = None, init_settings: List[String] = Nil, more_settings: List[String] = Nil, more_preferences: List[String] = Nil, verbose: Boolean = false, build_tags: List[String] = Nil, build_args: List[String] = Nil): List[(Process_Result, Path)] = { /* sanity checks */ if (File.eq(Path.explode("~~"), root)) error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand) for ((threads, _) <- multicore_list if threads < 1) error("Bad threads value < 1: " + threads) for ((_, processes) <- multicore_list if processes < 1) error("Bad processes value < 1: " + processes) if (heap < 100) error("Bad heap value < 100: " + heap) if (max_heap.isDefined && max_heap.get < heap) error("Bad max_heap value < heap: " + max_heap.get) System.getenv("ISABELLE_SETTINGS_PRESENT") match { case null | "" => case _ => error("Cannot run build_history within existing Isabelle settings environment") } /* checkout Isabelle + AFP repository */ def checkout(dir: Path, version: String): String = { val hg = Mercurial.repository(dir) hg.update(rev = version, clean = true) progress.echo_if(verbose, hg.log(version, options = "-l1")) hg.id(rev = version) } val isabelle_version = checkout(root, rev) val afp_repos = root + Path.explode("AFP") val afp_version = afp_rev.map(checkout(afp_repos, _)) val (afp_build_args, afp_sessions) = if (afp_rev.isEmpty) (Nil, Nil) else { val afp = AFP.init(options, afp_repos) (List("-d", "~~/AFP/thys"), afp.partition(afp_partition)) } /* main */ val other_isabelle = Other_Isabelle(root, isabelle_identifier = isabelle_identifier, user_home = user_home, progress = progress) val build_host = proper_string(hostname) getOrElse Isabelle_System.hostname() val build_history_date = Date.now() val build_group_id = build_host + ":" + build_history_date.time.ms var first_build = true for ((threads, processes) <- multicore_list) yield { /* init settings */ val component_settings = other_isabelle.init_components( components_base = components_base, catalogs = List("main", "optional")) other_isabelle.init_settings(component_settings ::: init_settings) other_isabelle.resolve_components(verbose) val ml_platform = augment_settings(other_isabelle, threads, arch_64, heap, max_heap, more_settings) File.write(other_isabelle.etc_preferences, cat_lines(more_preferences)) val isabelle_output = other_isabelle.isabelle_home_user + Path.explode("heaps") + Path.explode(other_isabelle.getenv("ML_IDENTIFIER")) val isabelle_output_log = isabelle_output + Path.explode("log") val isabelle_base_log = isabelle_output + Path.explode("../base_log") if (first_build) { other_isabelle.resolve_components(verbose) if (fresh) Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode("lib/classes")) other_isabelle.bash( "env PATH=\"" + File.bash_path(Path.explode("~~/lib/dummy_stty").expand) + ":$PATH\" " + "bin/isabelle jedit -b", redirect = true, echo = verbose).check for { tool <- List("ghc_setup", "ocaml_setup") if other_isabelle.getenv("ISABELLE_" + Word.uppercase(tool)) == "true" && (other_isabelle.isabelle_home + Path.explode("lib/Tools/" + tool)).is_file } other_isabelle(tool, echo = verbose) Isabelle_System.rm_tree(isabelle_base_log) } Isabelle_System.rm_tree(isabelle_output) Isabelle_System.mkdirs(isabelle_output) val log_path = other_isabelle.isabelle_home_user + Build_Log.log_subdir(build_history_date) + Build_Log.log_filename(Build_History.engine, build_history_date, List(build_host, ml_platform, "M" + threads) ::: build_tags) Isabelle_System.mkdirs(log_path.dir) val build_out = other_isabelle.isabelle_home_user + Path.explode("log/build.out") val build_out_progress = new File_Progress(build_out) build_out.file.delete /* build */ if (multicore_base && !first_build && isabelle_base_log.is_dir) Isabelle_System.copy_dir(isabelle_base_log, isabelle_output_log) val build_start = Date.now() val build_args1 = List("-v", "-j" + processes) ::: afp_build_args ::: build_args val build_isabelle = Other_Isabelle(root, isabelle_identifier = isabelle_identifier, user_home = user_home, progress = build_out_progress) val build_result = build_isabelle("build " + Bash.strings(build_args1 ::: afp_sessions), redirect = true, echo = true, strict = false) val build_end = Date.now() val build_info: Build_Log.Build_Info = Build_Log.Log_File(log_path.file_name, build_result.out_lines). parse_build_info(ml_statistics = true) /* output log */ val store = Sessions.store(options + "build_database_server=false") val meta_info = Properties.lines_nonempty(Build_Log.Prop.build_tags.name, build_tags) ::: Properties.lines_nonempty(Build_Log.Prop.build_args.name, build_args1) ::: List( Build_Log.Prop.build_group_id.name -> build_group_id, Build_Log.Prop.build_id.name -> (build_host + ":" + build_start.time.ms), Build_Log.Prop.build_engine.name -> Build_History.engine, Build_Log.Prop.build_host.name -> build_host, Build_Log.Prop.build_start.name -> Build_Log.print_date(build_start), Build_Log.Prop.build_end.name -> Build_Log.print_date(build_end), Build_Log.Prop.isabelle_version.name -> isabelle_version) ::: afp_version.map(Build_Log.Prop.afp_version.name -> _).toList build_out_progress.echo("Reading session build info ...") val session_build_info = build_info.finished_sessions.flatMap(session_name => { val database = isabelle_output + store.database(session_name) if (database.is_file) { using(SQLite.open_database(database))(db => { + val session_timing = + { + val props = store.read_session_timing(db, session_name) + val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse "1" + val timing = Markup.Timing_Properties.unapply(props) getOrElse Timing.zero + "Timing " + session_name + " (" + threads + " threads, " + timing.message_resources + ")" + } + val theory_timings = try { store.read_theory_timings(db, session_name).map(ps => Protocol.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps)) } catch { case ERROR(_) => Nil } val session_sources = store.read_build(db, session_name).map(_.sources) match { case Some(sources) if sources.length == SHA1.digest_length => List("Sources " + session_name + " " + sources) case _ => Nil } - theory_timings ::: session_sources + session_timing :: theory_timings ::: session_sources }) } else Nil }) build_out_progress.echo("Reading ML statistics ...") val ml_statistics = build_info.finished_sessions.flatMap(session_name => { val database = isabelle_output + store.database(session_name) val log_gz = isabelle_output + store.log_gz(session_name) val properties = if (database.is_file) { using(SQLite.open_database(database))(db => store.read_ml_statistics(db, session_name)) } else if (log_gz.is_file) { Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics } else Nil val trimmed_properties = if (ml_statistics_step <= 0) Nil else if (ml_statistics_step == 1) properties else { (for { (ps, i) <- properties.iterator.zipWithIndex if i % ml_statistics_step == 0 } yield ps).toList } trimmed_properties.map(ps => (Build_Log.SESSION_NAME -> session_name) :: ps) }) build_out_progress.echo("Reading error messages ...") val session_errors = build_info.failed_sessions.flatMap(session_name => { val database = isabelle_output + store.database(session_name) val errors = if (database.is_file) { try { using(SQLite.open_database(database))(db => store.read_errors(db, session_name)) } // column "errors" could be missing catch { case _: java.sql.SQLException => Nil } } else Nil errors.map(msg => List(Build_Log.SESSION_NAME -> session_name, Markup.CONTENT -> msg)) }) build_out_progress.echo("Reading heap sizes ...") val heap_sizes = build_info.finished_sessions.flatMap(session_name => { val heap = isabelle_output + Path.explode(session_name) if (heap.is_file) Some("Heap " + session_name + " (" + Value.Long(heap.file.length) + " bytes)") else None }) build_out_progress.echo("Writing log file " + log_path.ext("xz") + " ...") File.write_xz(log_path.ext("xz"), terminate_lines( Protocol.Meta_Info_Marker(meta_info) :: build_result.out_lines ::: session_build_info ::: ml_statistics.map(Protocol.ML_Statistics_Marker.apply) ::: session_errors.map(Protocol.Error_Message_Marker.apply) ::: heap_sizes), XZ.options(6)) /* next build */ if (multicore_base && first_build && isabelle_output_log.is_dir) Isabelle_System.copy_dir(isabelle_output_log, isabelle_base_log) Isabelle_System.rm_tree(isabelle_output) first_build = false (build_result, log_path.ext("xz")) } } /* command line entry point */ private object Multicore { private val Pat1 = """^(\d+)$""".r private val Pat2 = """^(\d+)x(\d+)$""".r def parse(s: String): (Int, Int) = s match { case Pat1(Value.Int(x)) => (x, 1) case Pat2(Value.Int(x), Value.Int(y)) => (x, y) case _ => error("Bad multicore configuration: " + quote(s)) } } def main(args: Array[String]) { Command_Line.tool { var afp_rev: Option[String] = None var multicore_base = false var components_base: Path = Components.default_components_base var heap: Option[Int] = None var max_heap: Option[Int] = None var multicore_list = List(default_multicore) var isabelle_identifier = default_isabelle_identifier var afp_partition = 0 var more_settings: List[String] = Nil var more_preferences: List[String] = Nil var fresh = false var hostname = "" var init_settings: List[String] = Nil var arch_64 = false var output_file = "" var rev = default_rev var ml_statistics_step = 1 var build_tags = List.empty[String] var user_home = default_user_home var verbose = false var exit_code = false val getopts = Getopts(""" Usage: Admin/build_history [OPTIONS] REPOSITORY [ARGS ...] Options are: -A REV include $ISABELLE_HOME/AFP repository at given revision -B first multicore build serves as base for scheduling information -C DIR base directory for Isabelle components (default: """ + Components.default_components_base + """) -H SIZE minimal ML heap in MB (default: """ + default_heap + """ for x86, """ + default_heap * 2 + """ for x86_64) -M MULTICORE multicore configurations (see below) -N NAME alternative ISABELLE_IDENTIFIER (default: """ + default_isabelle_identifier + """) -P NUMBER AFP partition number (0, 1, 2, default: 0=unrestricted) -U SIZE maximal ML heap in MB (default: unbounded) -e TEXT additional text for generated etc/settings -f fresh build of Isabelle/Scala components (recommended) -h NAME override local hostname -i TEXT initial text for generated etc/settings -m ARCH processor architecture (32=x86, 64=x86_64, default: x86) -o FILE output file for log names (default: stdout) -p TEXT additional text for generated etc/preferences -r REV update to revision (default: """ + default_rev + """) -s NUMBER step size for ML statistics (0=none, 1=all, n=step, default: 1) -t TAG free-form build tag (multiple occurrences possible) -u DIR alternative USER_HOME directory -v verbose -x return overall exit code from build processes Build Isabelle sessions from the history of another REPOSITORY clone, passing ARGS directly to its isabelle build tool. Each MULTICORE configuration consists of one or two numbers (default 1): THREADS or THREADSxPROCESSES, e.g. -M 1,2,4 or -M 1x4,2x2,4. """, "A:" -> (arg => afp_rev = Some(arg)), "B" -> (_ => multicore_base = true), "C:" -> (arg => components_base = Path.explode(arg)), "H:" -> (arg => heap = Some(Value.Int.parse(arg))), "M:" -> (arg => multicore_list = space_explode(',', arg).map(Multicore.parse)), "N:" -> (arg => isabelle_identifier = arg), "P:" -> (arg => afp_partition = Value.Int.parse(arg)), "U:" -> (arg => max_heap = Some(Value.Int.parse(arg))), "e:" -> (arg => more_settings = more_settings ::: List(arg)), "f" -> (_ => fresh = true), "h:" -> (arg => hostname = arg), "i:" -> (arg => init_settings = init_settings ::: List(arg)), "m:" -> { case "32" | "x86" => arch_64 = false case "64" | "x86_64" => arch_64 = true case bad => error("Bad processor architecture: " + quote(bad)) }, "o:" -> (arg => output_file = arg), "p:" -> (arg => more_preferences = more_preferences ::: List(arg)), "r:" -> (arg => rev = arg), "s:" -> (arg => ml_statistics_step = Value.Int.parse(arg)), "t:" -> (arg => build_tags = build_tags ::: List(arg)), "u:" -> (arg => user_home = Path.explode(arg)), "v" -> (_ => verbose = true), "x" -> (_ => exit_code = true)) val more_args = getopts(args) val (root, build_args) = more_args match { case root :: build_args => (Path.explode(root), build_args) case _ => getopts.usage() } val progress = new Console_Progress(stderr = true) val results = build_history(Options.init(), root, user_home = user_home, progress = progress, rev = rev, afp_rev = afp_rev, afp_partition = afp_partition, isabelle_identifier = isabelle_identifier, ml_statistics_step = ml_statistics_step, components_base = components_base, fresh = fresh, hostname = hostname, multicore_base = multicore_base, multicore_list = multicore_list, arch_64 = arch_64, heap = heap.getOrElse(if (arch_64) default_heap * 2 else default_heap), max_heap = max_heap, init_settings = init_settings, more_settings = more_settings, more_preferences = more_preferences, verbose = verbose, build_tags = build_tags, build_args = build_args) if (output_file == "") { for ((_, log_path) <- results) Output.writeln(log_path.implode, stdout = true) } else { File.write(Path.explode(output_file), cat_lines(for ((_, log_path) <- results) yield log_path.implode)) } val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc } if (rc != 0 && exit_code) sys.exit(rc) } } /** remote build_history -- via command-line **/ def remote_build_history( ssh: SSH.Session, isabelle_repos_self: Path, isabelle_repos_other: Path, isabelle_repos_source: String = Isabelle_Cronjob.isabelle_repos_source, afp_repos_source: String = AFP.repos_source, isabelle_identifier: String = "remote_build_history", self_update: Boolean = false, progress: Progress = new Progress, rev: String = "", afp_rev: Option[String] = None, options: String = "", args: String = ""): List[(String, Bytes)] = { /* Isabelle self repository */ val self_hg = Mercurial.setup_repository(isabelle_repos_source, isabelle_repos_self, ssh = ssh) def execute(cmd: String, args: String, echo: Boolean = false, strict: Boolean = true): Unit = ssh.execute( Isabelle_System.export_isabelle_identifier(isabelle_identifier) + ssh.bash_path(isabelle_repos_self + Path.explode(cmd)) + " " + args, progress_stdout = progress.echo_if(echo, _), progress_stderr = progress.echo_if(echo, _), strict = strict).check if (self_update) { val hg = Mercurial.repository(Path.explode("~~")) hg.push(self_hg.root_url, force = true) self_hg.update(rev = hg.parent(), clean = true) execute("bin/isabelle", "components -I") execute("bin/isabelle", "components -a", echo = true) execute("Admin/build", "jars_fresh") } val rev_id = self_hg.id(rev) /* Isabelle other + AFP repository */ if (Mercurial.is_repository(isabelle_repos_other, ssh = ssh)) { ssh.rm_tree(isabelle_repos_other) } val other_hg = Mercurial.clone_repository( ssh.bash_path(isabelle_repos_self), isabelle_repos_other, rev = rev_id, ssh = ssh) val afp_options = if (afp_rev.isEmpty) "" else { val afp_repos = isabelle_repos_other + Path.explode("AFP") val afp_hg = Mercurial.setup_repository(afp_repos_source, afp_repos, ssh = ssh) " -A " + Bash.string(afp_rev.get) } /* Admin/build_history */ ssh.with_tmp_dir(tmp_dir => { val output_file = tmp_dir + Path.explode("output") execute("Admin/build_history", "-o " + ssh.bash_path(output_file) + (if (rev == "") "" else " -r " + Bash.string(rev_id)) + " " + options + afp_options + " " + ssh.bash_path(isabelle_repos_other) + " " + args, echo = true, strict = false) for (line <- split_lines(ssh.read(output_file))) yield { val log = Path.explode(line) val bytes = ssh.read_bytes(log) ssh.rm(log) (log.file_name, bytes) } }) } } 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,693 +1,696 @@ /* 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) 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 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 } } 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 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.String("threads") + } object ML_Statistics extends Properties_Function("ML_statistics") object Task_Statistics extends Properties_Function("task_statistics") object Loading_Theory extends Name_Function("loading_theory") object Build_Session_Finished extends Function("build_session_finished") object Protocol_Handler extends Name_Function("protocol_handler") 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)] = props match { case List(PROPERTY, (NAME, name), (ID, id)) => Some((name, id)) 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)) }