update theory sources based on PIDE markup;
authorwenzelm
Mon Dec 31 13:07:24 2018 +0100 (18 months ago)
changeset 69557e72360fef69a
parent 69556 0a38f23ca4c5
child 69558 101ee69cba49
update theory sources based on PIDE markup;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/System/isabelle_tool.scala
src/Pure/Tools/update.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/PIDE/markup.ML	Mon Dec 31 12:02:31 2018 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Mon Dec 31 13:07:24 2018 +0100
     1.3 @@ -45,6 +45,7 @@
     1.4    val refN: string
     1.5    val completionN: string val completion: T
     1.6    val no_completionN: string val no_completion: T
     1.7 +  val updateN: string val update: T
     1.8    val lineN: string
     1.9    val end_lineN: string
    1.10    val offsetN: string
    1.11 @@ -336,6 +337,8 @@
    1.12  val (completionN, completion) = markup_elem "completion";
    1.13  val (no_completionN, no_completion) = markup_elem "no_completion";
    1.14  
    1.15 +val (updateN, update) = markup_elem "update";
    1.16 +
    1.17  
    1.18  (* position *)
    1.19  
     2.1 --- a/src/Pure/PIDE/markup.scala	Mon Dec 31 12:02:31 2018 +0100
     2.2 +++ b/src/Pure/PIDE/markup.scala	Mon Dec 31 13:07:24 2018 +0100
     2.3 @@ -115,6 +115,8 @@
     2.4    val COMPLETION = "completion"
     2.5    val NO_COMPLETION = "no_completion"
     2.6  
     2.7 +  val UPDATE = "update"
     2.8 +
     2.9  
    2.10    /* position */
    2.11  
     3.1 --- a/src/Pure/System/isabelle_tool.scala	Mon Dec 31 12:02:31 2018 +0100
     3.2 +++ b/src/Pure/System/isabelle_tool.scala	Mon Dec 31 13:07:24 2018 +0100
     3.3 @@ -155,6 +155,7 @@
     3.4    Present.isabelle_tool,
     3.5    Profiling_Report.isabelle_tool,
     3.6    Server.isabelle_tool,
     3.7 +  Update.isabelle_tool,
     3.8    Update_Cartouches.isabelle_tool,
     3.9    Update_Comments.isabelle_tool,
    3.10    Update_Header.isabelle_tool,
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Tools/update.scala	Mon Dec 31 13:07:24 2018 +0100
     4.3 @@ -0,0 +1,132 @@
     4.4 +/*  Title:      Pure/Tools/update.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Update theory sources based on PIDE markup.
     4.8 +*/
     4.9 +
    4.10 +package isabelle
    4.11 +
    4.12 +
    4.13 +object Update
    4.14 +{
    4.15 +  def update(options: Options, logic: String,
    4.16 +    progress: Progress = No_Progress,
    4.17 +    log: Logger = No_Logger,
    4.18 +    dirs: List[Path] = Nil,
    4.19 +    select_dirs: List[Path] = Nil,
    4.20 +    system_mode: Boolean = false,
    4.21 +    selection: Sessions.Selection = Sessions.Selection.empty)
    4.22 +  {
    4.23 +    Build.build_logic(options, logic, build_heap = true, progress = progress,
    4.24 +      dirs = dirs ::: select_dirs, system_mode = system_mode, strict = true)
    4.25 +
    4.26 +    val dump_options = Dump.make_options(options)
    4.27 +
    4.28 +    val deps =
    4.29 +      Dump.dependencies(dump_options, progress = progress,
    4.30 +        dirs = dirs, select_dirs = select_dirs, selection = selection)._1
    4.31 +
    4.32 +    val resources =
    4.33 +      Headless.Resources.make(dump_options, logic, progress = progress, log = log,
    4.34 +        session_dirs = dirs ::: select_dirs,
    4.35 +        include_sessions = deps.sessions_structure.imports_topological_order)
    4.36 +
    4.37 +    def update_xml(xml: XML.Body): XML.Body =
    4.38 +      xml flatMap {
    4.39 +        case XML.Wrapped_Elem(markup, body1, body2) =>
    4.40 +          if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2)
    4.41 +        case XML.Elem(_, body) => update_xml(body)
    4.42 +        case t => List(t)
    4.43 +      }
    4.44 +
    4.45 +    Dump.session(deps, resources, progress = progress,
    4.46 +      process_theory =
    4.47 +        (deps: Sessions.Deps, snapshot: Document.Snapshot, status: Document_Status.Node_Status) =>
    4.48 +        {
    4.49 +          for ((node_name, node) <- snapshot.nodes) {
    4.50 +            val xml =
    4.51 +              snapshot.state.markup_to_XML(snapshot.version, node_name,
    4.52 +                Text.Range.full, Markup.Elements(Markup.UPDATE))
    4.53 +
    4.54 +            val source1 = Symbol.encode(XML.content(update_xml(xml)))
    4.55 +            if (source1 != Symbol.encode(node.source)) {
    4.56 +              progress.echo("Updating " + node_name.path)
    4.57 +              File.write(node_name.path, source1)
    4.58 +            }
    4.59 +          }
    4.60 +        })
    4.61 +  }
    4.62 +
    4.63 +
    4.64 +  /* Isabelle tool wrapper */
    4.65 +
    4.66 +  val isabelle_tool =
    4.67 +    Isabelle_Tool("update", "update theory sources based on PIDE markup", args =>
    4.68 +    {
    4.69 +      var base_sessions: List[String] = Nil
    4.70 +      var select_dirs: List[Path] = Nil
    4.71 +      var requirements = false
    4.72 +      var exclude_session_groups: List[String] = Nil
    4.73 +      var all_sessions = false
    4.74 +      var dirs: List[Path] = Nil
    4.75 +      var session_groups: List[String] = Nil
    4.76 +      var logic = Isabelle_System.getenv("ISABELLE_LOGIC")
    4.77 +      var options = Options.init()
    4.78 +      var system_mode = false
    4.79 +      var verbose = false
    4.80 +      var exclude_sessions: List[String] = Nil
    4.81 +
    4.82 +      val getopts = Getopts("""
    4.83 +Usage: isabelle update [OPTIONS] [SESSIONS ...]
    4.84 +
    4.85 +  Options are:
    4.86 +    -B NAME      include session NAME and all descendants
    4.87 +    -D DIR       include session directory and select its sessions
    4.88 +    -R           operate on requirements of selected sessions
    4.89 +    -X NAME      exclude sessions from group NAME and all descendants
    4.90 +    -a           select all sessions
    4.91 +    -d DIR       include session directory
    4.92 +    -g NAME      select session group NAME
    4.93 +    -l NAME      logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """)
    4.94 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    4.95 +    -s           system build mode for logic image
    4.96 +    -u OPT       overide update option: shortcut for "-o update_OPT"
    4.97 +    -v           verbose
    4.98 +    -x NAME      exclude session NAME and all descendants
    4.99 +
   4.100 +  Update theory sources based on PIDE markup.
   4.101 +""",
   4.102 +      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
   4.103 +      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   4.104 +      "R" -> (_ => requirements = true),
   4.105 +      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   4.106 +      "a" -> (_ => all_sessions = true),
   4.107 +      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   4.108 +      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   4.109 +      "l:" -> (arg => logic = arg),
   4.110 +      "o:" -> (arg => options = options + arg),
   4.111 +      "s" -> (_ => system_mode = true),
   4.112 +      "u:" -> (arg => options = options + ("update_" + arg)),
   4.113 +      "v" -> (_ => verbose = true),
   4.114 +      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   4.115 +
   4.116 +      val sessions = getopts(args)
   4.117 +
   4.118 +      val progress = new Console_Progress(verbose = verbose)
   4.119 +
   4.120 +      progress.interrupt_handler {
   4.121 +        update(options, logic,
   4.122 +          progress = progress,
   4.123 +          dirs = dirs,
   4.124 +          select_dirs = select_dirs,
   4.125 +          selection = Sessions.Selection(
   4.126 +            requirements = requirements,
   4.127 +            all_sessions = all_sessions,
   4.128 +            base_sessions = base_sessions,
   4.129 +            exclude_session_groups = exclude_session_groups,
   4.130 +            exclude_sessions = exclude_sessions,
   4.131 +            session_groups = session_groups,
   4.132 +            sessions = sessions))
   4.133 +      }
   4.134 +    })
   4.135 +}
     5.1 --- a/src/Pure/build-jars	Mon Dec 31 12:02:31 2018 +0100
     5.2 +++ b/src/Pure/build-jars	Mon Dec 31 13:07:24 2018 +0100
     5.3 @@ -160,6 +160,7 @@
     5.4    Tools/simplifier_trace.scala
     5.5    Tools/spell_checker.scala
     5.6    Tools/task_statistics.scala
     5.7 +  Tools/update.scala
     5.8    Tools/update_cartouches.scala
     5.9    Tools/update_comments.scala
    5.10    Tools/update_header.scala