# HG changeset patch # User wenzelm # Date 1546258044 -3600 # Node ID e72360fef69a6117607adc1a4da28a60d443c470 # Parent 0a38f23ca4c54e73b040ef441c22b82583e98482 update theory sources based on PIDE markup; diff -r 0a38f23ca4c5 -r e72360fef69a src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Mon Dec 31 12:02:31 2018 +0100 +++ b/src/Pure/PIDE/markup.ML Mon Dec 31 13:07:24 2018 +0100 @@ -45,6 +45,7 @@ val refN: string val completionN: string val completion: T val no_completionN: string val no_completion: T + val updateN: string val update: T val lineN: string val end_lineN: string val offsetN: string @@ -336,6 +337,8 @@ val (completionN, completion) = markup_elem "completion"; val (no_completionN, no_completion) = markup_elem "no_completion"; +val (updateN, update) = markup_elem "update"; + (* position *) diff -r 0a38f23ca4c5 -r e72360fef69a src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Mon Dec 31 12:02:31 2018 +0100 +++ b/src/Pure/PIDE/markup.scala Mon Dec 31 13:07:24 2018 +0100 @@ -115,6 +115,8 @@ val COMPLETION = "completion" val NO_COMPLETION = "no_completion" + val UPDATE = "update" + /* position */ diff -r 0a38f23ca4c5 -r e72360fef69a src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Mon Dec 31 12:02:31 2018 +0100 +++ b/src/Pure/System/isabelle_tool.scala Mon Dec 31 13:07:24 2018 +0100 @@ -155,6 +155,7 @@ Present.isabelle_tool, Profiling_Report.isabelle_tool, Server.isabelle_tool, + Update.isabelle_tool, Update_Cartouches.isabelle_tool, Update_Comments.isabelle_tool, Update_Header.isabelle_tool, diff -r 0a38f23ca4c5 -r e72360fef69a src/Pure/Tools/update.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/update.scala Mon Dec 31 13:07:24 2018 +0100 @@ -0,0 +1,132 @@ +/* Title: Pure/Tools/update.scala + Author: Makarius + +Update theory sources based on PIDE markup. +*/ + +package isabelle + + +object Update +{ + def update(options: Options, logic: String, + progress: Progress = No_Progress, + log: Logger = No_Logger, + dirs: List[Path] = Nil, + select_dirs: List[Path] = Nil, + system_mode: Boolean = false, + selection: Sessions.Selection = Sessions.Selection.empty) + { + Build.build_logic(options, logic, build_heap = true, progress = progress, + dirs = dirs ::: select_dirs, system_mode = system_mode, strict = true) + + val dump_options = Dump.make_options(options) + + val deps = + Dump.dependencies(dump_options, progress = progress, + dirs = dirs, select_dirs = select_dirs, selection = selection)._1 + + val resources = + Headless.Resources.make(dump_options, logic, progress = progress, log = log, + session_dirs = dirs ::: select_dirs, + include_sessions = deps.sessions_structure.imports_topological_order) + + def update_xml(xml: XML.Body): XML.Body = + xml flatMap { + case XML.Wrapped_Elem(markup, body1, body2) => + if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2) + case XML.Elem(_, body) => update_xml(body) + case t => List(t) + } + + Dump.session(deps, resources, progress = progress, + process_theory = + (deps: Sessions.Deps, snapshot: Document.Snapshot, status: Document_Status.Node_Status) => + { + for ((node_name, node) <- snapshot.nodes) { + val xml = + snapshot.state.markup_to_XML(snapshot.version, node_name, + Text.Range.full, Markup.Elements(Markup.UPDATE)) + + val source1 = Symbol.encode(XML.content(update_xml(xml))) + if (source1 != Symbol.encode(node.source)) { + progress.echo("Updating " + node_name.path) + File.write(node_name.path, source1) + } + } + }) + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = + Isabelle_Tool("update", "update theory sources based on PIDE markup", args => + { + var base_sessions: List[String] = Nil + var select_dirs: List[Path] = Nil + var requirements = false + var exclude_session_groups: List[String] = Nil + var all_sessions = false + var dirs: List[Path] = Nil + var session_groups: List[String] = Nil + var logic = Isabelle_System.getenv("ISABELLE_LOGIC") + var options = Options.init() + var system_mode = false + var verbose = false + var exclude_sessions: List[String] = Nil + + val getopts = Getopts(""" +Usage: isabelle update [OPTIONS] [SESSIONS ...] + + Options are: + -B NAME include session NAME and all descendants + -D DIR include session directory and select its sessions + -R operate on requirements of selected sessions + -X NAME exclude sessions from group NAME and all descendants + -a select all sessions + -d DIR include session directory + -g NAME select session group NAME + -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -s system build mode for logic image + -u OPT overide update option: shortcut for "-o update_OPT" + -v verbose + -x NAME exclude session NAME and all descendants + + Update theory sources based on PIDE markup. +""", + "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), + "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), + "R" -> (_ => requirements = true), + "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), + "a" -> (_ => all_sessions = true), + "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), + "g:" -> (arg => session_groups = session_groups ::: List(arg)), + "l:" -> (arg => logic = arg), + "o:" -> (arg => options = options + arg), + "s" -> (_ => system_mode = true), + "u:" -> (arg => options = options + ("update_" + arg)), + "v" -> (_ => verbose = true), + "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) + + val sessions = getopts(args) + + val progress = new Console_Progress(verbose = verbose) + + progress.interrupt_handler { + update(options, logic, + progress = progress, + dirs = dirs, + select_dirs = select_dirs, + selection = Sessions.Selection( + requirements = requirements, + all_sessions = all_sessions, + base_sessions = base_sessions, + exclude_session_groups = exclude_session_groups, + exclude_sessions = exclude_sessions, + session_groups = session_groups, + sessions = sessions)) + } + }) +} diff -r 0a38f23ca4c5 -r e72360fef69a src/Pure/build-jars --- a/src/Pure/build-jars Mon Dec 31 12:02:31 2018 +0100 +++ b/src/Pure/build-jars Mon Dec 31 13:07:24 2018 +0100 @@ -160,6 +160,7 @@ Tools/simplifier_trace.scala Tools/spell_checker.scala Tools/task_statistics.scala + Tools/update.scala Tools/update_cartouches.scala Tools/update_comments.scala Tools/update_header.scala