1/*  Title:      Pure/Tools/update.scala
2    Author:     Makarius
3
4Update theory sources based on PIDE markup.
5*/
6
7package isabelle
8
9
10object Update
11{
12  def update(options: Options, logic: String,
13    progress: Progress = No_Progress,
14    log: Logger = No_Logger,
15    dirs: List[Path] = Nil,
16    select_dirs: List[Path] = Nil,
17    selection: Sessions.Selection = Sessions.Selection.empty)
18  {
19    val context =
20      Dump.Context(options, progress = progress, dirs = dirs, select_dirs = select_dirs,
21        selection = selection, skip_base = true)
22
23    context.build_logic(logic)
24
25    val path_cartouches = context.options.bool("update_path_cartouches")
26
27    def update_xml(xml: XML.Body): XML.Body =
28      xml flatMap {
29        case XML.Wrapped_Elem(markup, body1, body2) =>
30          if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2)
31        case XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), body)
32        if path_cartouches =>
33          Token.read_embedded(Keyword.Keywords.empty, XML.content(body)) match {
34            case Some(tok) => List(XML.Text(Symbol.cartouche(tok.content)))
35            case None => update_xml(body)
36          }
37        case XML.Elem(_, body) => update_xml(body)
38        case t => List(t)
39      }
40
41    context.sessions(logic, log = log).foreach(_.process((args: Dump.Args) =>
42      {
43        progress.echo("Processing theory " + args.print_node + " ...")
44
45        val snapshot = args.snapshot
46        for ((node_name, node) <- snapshot.nodes) {
47          val xml =
48            snapshot.state.markup_to_XML(snapshot.version, node_name,
49              Text.Range.full, Markup.Elements(Markup.UPDATE, Markup.LANGUAGE))
50
51          val source1 = Symbol.encode(XML.content(update_xml(xml)))
52          if (source1 != Symbol.encode(node.source)) {
53            progress.echo("Updating " + node_name.path)
54            File.write(node_name.path, source1)
55          }
56        }
57      }))
58
59    context.check_errors
60  }
61
62
63  /* Isabelle tool wrapper */
64
65  val isabelle_tool =
66    Isabelle_Tool("update", "update theory sources based on PIDE markup", args =>
67    {
68      var base_sessions: List[String] = Nil
69      var select_dirs: List[Path] = Nil
70      var requirements = false
71      var exclude_session_groups: List[String] = Nil
72      var all_sessions = false
73      var dirs: List[Path] = Nil
74      var session_groups: List[String] = Nil
75      var logic = Dump.default_logic
76      var options = Options.init()
77      var verbose = false
78      var exclude_sessions: List[String] = Nil
79
80      val getopts = Getopts("""
81Usage: isabelle update [OPTIONS] [SESSIONS ...]
82
83  Options are:
84    -B NAME      include session NAME and all descendants
85    -D DIR       include session directory and select its sessions
86    -R           operate on requirements of selected sessions
87    -X NAME      exclude sessions from group NAME and all descendants
88    -a           select all sessions
89    -b NAME      base logic image (default """ + isabelle.quote(Dump.default_logic) + """)
90    -d DIR       include session directory
91    -g NAME      select session group NAME
92    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
93    -u OPT       overide update option: shortcut for "-o update_OPT"
94    -v           verbose
95    -x NAME      exclude session NAME and all descendants
96
97  Update theory sources based on PIDE markup.
98""",
99      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
100      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
101      "R" -> (_ => requirements = true),
102      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
103      "a" -> (_ => all_sessions = true),
104      "b:" -> (arg => logic = arg),
105      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
106      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
107      "o:" -> (arg => options = options + arg),
108      "u:" -> (arg => options = options + ("update_" + arg)),
109      "v" -> (_ => verbose = true),
110      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
111
112      val sessions = getopts(args)
113
114      val progress = new Console_Progress(verbose = verbose)
115
116      progress.interrupt_handler {
117        update(options, logic,
118          progress = progress,
119          dirs = dirs,
120          select_dirs = select_dirs,
121          selection = Sessions.Selection(
122            requirements = requirements,
123            all_sessions = all_sessions,
124            base_sessions = base_sessions,
125            exclude_session_groups = exclude_session_groups,
126            exclude_sessions = exclude_sessions,
127            session_groups = session_groups,
128            sessions = sessions))
129      }
130    })
131}
132