35 } |
35 } |
36 case XML.Elem(_, body) => update_xml(body) |
36 case XML.Elem(_, body) => update_xml(body) |
37 case t => List(t) |
37 case t => List(t) |
38 } |
38 } |
39 |
39 |
40 context.sessions(logic, log = log).foreach(_.process((args: Dump.Args) => { |
40 context.sessions(logic, log = log).foreach(_.process { (args: Dump.Args) => |
41 progress.echo("Processing theory " + args.print_node + " ...") |
41 progress.echo("Processing theory " + args.print_node + " ...") |
42 |
42 |
43 val snapshot = args.snapshot |
43 val snapshot = args.snapshot |
44 for (node_name <- snapshot.node_files) { |
44 for (node_name <- snapshot.node_files) { |
45 val node = snapshot.get_node(node_name) |
45 val node = snapshot.get_node(node_name) |
51 if (source1 != Symbol.encode(node.source)) { |
51 if (source1 != Symbol.encode(node.source)) { |
52 progress.echo("Updating " + node_name.path) |
52 progress.echo("Updating " + node_name.path) |
53 File.write(node_name.path, source1) |
53 File.write(node_name.path, source1) |
54 } |
54 } |
55 } |
55 } |
56 })) |
56 }) |
57 |
57 |
58 context.check_errors |
58 context.check_errors |
59 } |
59 } |
60 |
60 |
61 |
61 |
62 /* Isabelle tool wrapper */ |
62 /* Isabelle tool wrapper */ |
63 |
63 |
64 val isabelle_tool = |
64 val isabelle_tool = |
65 Isabelle_Tool("update", "update theory sources based on PIDE markup", Scala_Project.here, |
65 Isabelle_Tool("update", "update theory sources based on PIDE markup", Scala_Project.here, |
66 args => { |
66 { args => |
67 var base_sessions: List[String] = Nil |
67 var base_sessions: List[String] = Nil |
68 var select_dirs: List[Path] = Nil |
68 var select_dirs: List[Path] = Nil |
69 var requirements = false |
69 var requirements = false |
70 var exclude_session_groups: List[String] = Nil |
70 var exclude_session_groups: List[String] = Nil |
71 var all_sessions = false |
71 var all_sessions = false |
72 var dirs: List[Path] = Nil |
72 var dirs: List[Path] = Nil |
73 var session_groups: List[String] = Nil |
73 var session_groups: List[String] = Nil |
74 var logic = Dump.default_logic |
74 var logic = Dump.default_logic |
75 var options = Options.init() |
75 var options = Options.init() |
76 var verbose = false |
76 var verbose = false |
77 var exclude_sessions: List[String] = Nil |
77 var exclude_sessions: List[String] = Nil |
78 |
78 |
79 val getopts = Getopts(""" |
79 val getopts = Getopts(""" |
80 Usage: isabelle update [OPTIONS] [SESSIONS ...] |
80 Usage: isabelle update [OPTIONS] [SESSIONS ...] |
81 |
81 |
82 Options are: |
82 Options are: |
83 -B NAME include session NAME and all descendants |
83 -B NAME include session NAME and all descendants |
84 -D DIR include session directory and select its sessions |
84 -D DIR include session directory and select its sessions |
93 -v verbose |
93 -v verbose |
94 -x NAME exclude session NAME and all descendants |
94 -x NAME exclude session NAME and all descendants |
95 |
95 |
96 Update theory sources based on PIDE markup. |
96 Update theory sources based on PIDE markup. |
97 """, |
97 """, |
98 "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), |
98 "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), |
99 "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), |
99 "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), |
100 "R" -> (_ => requirements = true), |
100 "R" -> (_ => requirements = true), |
101 "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), |
101 "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), |
102 "a" -> (_ => all_sessions = true), |
102 "a" -> (_ => all_sessions = true), |
103 "b:" -> (arg => logic = arg), |
103 "b:" -> (arg => logic = arg), |
104 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
104 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
105 "g:" -> (arg => session_groups = session_groups ::: List(arg)), |
105 "g:" -> (arg => session_groups = session_groups ::: List(arg)), |
106 "o:" -> (arg => options = options + arg), |
106 "o:" -> (arg => options = options + arg), |
107 "u:" -> (arg => options = options + ("update_" + arg)), |
107 "u:" -> (arg => options = options + ("update_" + arg)), |
108 "v" -> (_ => verbose = true), |
108 "v" -> (_ => verbose = true), |
109 "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) |
109 "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) |
110 |
110 |
111 val sessions = getopts(args) |
111 val sessions = getopts(args) |
112 |
112 |
113 val progress = new Console_Progress(verbose = verbose) |
113 val progress = new Console_Progress(verbose = verbose) |
114 |
114 |
115 progress.interrupt_handler { |
115 progress.interrupt_handler { |
116 update(options, logic, |
116 update(options, logic, |
117 progress = progress, |
117 progress = progress, |
118 dirs = dirs, |
118 dirs = dirs, |
119 select_dirs = select_dirs, |
119 select_dirs = select_dirs, |
120 selection = Sessions.Selection( |
120 selection = Sessions.Selection( |
121 requirements = requirements, |
121 requirements = requirements, |
122 all_sessions = all_sessions, |
122 all_sessions = all_sessions, |
123 base_sessions = base_sessions, |
123 base_sessions = base_sessions, |
124 exclude_session_groups = exclude_session_groups, |
124 exclude_session_groups = exclude_session_groups, |
125 exclude_sessions = exclude_sessions, |
125 exclude_sessions = exclude_sessions, |
126 session_groups = session_groups, |
126 session_groups = session_groups, |
127 sessions = sessions)) |
127 sessions = sessions)) |
128 } |
128 } |
129 }) |
129 }) |
130 } |
130 } |