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