|
1 /* Title: Pure/Tools/dump.scala |
|
2 Author: Makarius |
|
3 |
|
4 Dump build database produced by PIDE session. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object Dump |
|
11 { |
|
12 def dump(options: Options, logic: String, |
|
13 consume: Thy_Resources.Theories_Result => Unit = _ => (), |
|
14 progress: Progress = No_Progress, |
|
15 log: Logger = No_Logger, |
|
16 dirs: List[Path] = Nil, |
|
17 select_dirs: List[Path] = Nil, |
|
18 verbose: Boolean = false, |
|
19 system_mode: Boolean = false, |
|
20 selection: Sessions.Selection = Sessions.Selection.empty): Process_Result = |
|
21 { |
|
22 if (Build.build_logic(options, logic, progress = progress, dirs = dirs, |
|
23 system_mode = system_mode) != 0) error(logic + " FAILED") |
|
24 |
|
25 val dump_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", false) |
|
26 |
|
27 val deps = |
|
28 Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs). |
|
29 selection_deps(selection) |
|
30 |
|
31 val session = |
|
32 Thy_Resources.start_session(dump_options, logic, session_dirs = dirs, |
|
33 include_sessions = deps.sessions_structure.imports_topological_order, |
|
34 progress = progress, log = log) |
|
35 |
|
36 val theories = deps.all_known.theory_graph.topological_order.map(_.theory) |
|
37 val theories_result = session.use_theories(theories, progress = progress) |
|
38 |
|
39 try { consume(theories_result) } |
|
40 catch { case exn: Throwable => session.stop (); throw exn } |
|
41 |
|
42 session.stop() |
|
43 } |
|
44 |
|
45 |
|
46 /* Isabelle tool wrapper */ |
|
47 |
|
48 val isabelle_tool = |
|
49 Isabelle_Tool("dump", "dump build database produced by PIDE session.", args => |
|
50 { |
|
51 var base_sessions: List[String] = Nil |
|
52 var select_dirs: List[Path] = Nil |
|
53 var requirements = false |
|
54 var exclude_session_groups: List[String] = Nil |
|
55 var all_sessions = false |
|
56 var dirs: List[Path] = Nil |
|
57 var session_groups: List[String] = Nil |
|
58 var logic = Isabelle_System.getenv("ISABELLE_LOGIC") |
|
59 var options = Options.init() |
|
60 var system_mode = false |
|
61 var verbose = false |
|
62 var exclude_sessions: List[String] = Nil |
|
63 |
|
64 val getopts = Getopts(""" |
|
65 Usage: isabelle dump [OPTIONS] [SESSIONS ...] |
|
66 |
|
67 Options are: |
|
68 -B NAME include session NAME and all descendants |
|
69 -D DIR include session directory and select its sessions |
|
70 -R operate on requirements of selected sessions |
|
71 -X NAME exclude sessions from group NAME and all descendants |
|
72 -a select all sessions |
|
73 -d DIR include session directory |
|
74 -g NAME select session group NAME |
|
75 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) |
|
76 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
77 -s system build mode for logic image |
|
78 -v verbose |
|
79 -x NAME exclude session NAME and all descendants |
|
80 |
|
81 Dump build database (PIDE markup etc.) based on dynamic session.""", |
|
82 "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), |
|
83 "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), |
|
84 "R" -> (_ => requirements = true), |
|
85 "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), |
|
86 "a" -> (_ => all_sessions = true), |
|
87 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
|
88 "l:" -> (arg => logic = arg), |
|
89 "g:" -> (arg => session_groups = session_groups ::: List(arg)), |
|
90 "o:" -> (arg => options = options + arg), |
|
91 "s" -> (_ => system_mode = true), |
|
92 "v" -> (_ => verbose = true), |
|
93 "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) |
|
94 |
|
95 val sessions = getopts(args) |
|
96 |
|
97 val progress = new Console_Progress(verbose = verbose) |
|
98 |
|
99 def consume(theories_result: Thy_Resources.Theories_Result) |
|
100 { |
|
101 // FIXME |
|
102 for ((node, _) <- theories_result.nodes) progress.echo(node.toString) |
|
103 } |
|
104 |
|
105 val result = |
|
106 dump(options, logic, |
|
107 consume = consume _, |
|
108 progress = progress, |
|
109 dirs = dirs, |
|
110 select_dirs = select_dirs, |
|
111 verbose = verbose, |
|
112 selection = Sessions.Selection( |
|
113 requirements = requirements, |
|
114 all_sessions = all_sessions, |
|
115 base_sessions = base_sessions, |
|
116 exclude_session_groups = exclude_session_groups, |
|
117 exclude_sessions = exclude_sessions, |
|
118 session_groups = session_groups, |
|
119 sessions = sessions)) |
|
120 |
|
121 progress.echo(result.timing.message_resources) |
|
122 |
|
123 sys.exit(result.rc) |
|
124 }) |
|
125 } |