66 var requirements = false |
66 var requirements = false |
67 var exclude_session_groups: List[String] = Nil |
67 var exclude_session_groups: List[String] = Nil |
68 var all_sessions = false |
68 var all_sessions = false |
69 var dirs: List[Path] = Nil |
69 var dirs: List[Path] = Nil |
70 var session_groups: List[String] = Nil |
70 var session_groups: List[String] = Nil |
71 var logic = Isabelle_System.getenv("ISABELLE_LOGIC") |
71 var logic = Dump.default_logic |
72 var options = Options.init() |
72 var options = Options.init() |
73 var verbose = false |
73 var verbose = false |
74 var exclude_sessions: List[String] = Nil |
74 var exclude_sessions: List[String] = Nil |
75 |
75 |
76 val getopts = Getopts(""" |
76 val getopts = Getopts(""" |
80 -B NAME include session NAME and all descendants |
80 -B NAME include session NAME and all descendants |
81 -D DIR include session directory and select its sessions |
81 -D DIR include session directory and select its sessions |
82 -R operate on requirements of selected sessions |
82 -R operate on requirements of selected sessions |
83 -X NAME exclude sessions from group NAME and all descendants |
83 -X NAME exclude sessions from group NAME and all descendants |
84 -a select all sessions |
84 -a select all sessions |
|
85 -b NAME base logic image (default """ + isabelle.quote(Dump.default_logic) + """) |
85 -d DIR include session directory |
86 -d DIR include session directory |
86 -g NAME select session group NAME |
87 -g NAME select session group NAME |
87 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) |
|
88 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
88 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
89 -u OPT overide update option: shortcut for "-o update_OPT" |
89 -u OPT overide update option: shortcut for "-o update_OPT" |
90 -v verbose |
90 -v verbose |
91 -x NAME exclude session NAME and all descendants |
91 -x NAME exclude session NAME and all descendants |
92 |
92 |
95 "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), |
95 "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), |
96 "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), |
96 "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), |
97 "R" -> (_ => requirements = true), |
97 "R" -> (_ => requirements = true), |
98 "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), |
98 "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), |
99 "a" -> (_ => all_sessions = true), |
99 "a" -> (_ => all_sessions = true), |
|
100 "b:" -> (arg => logic = arg), |
100 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
101 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
101 "g:" -> (arg => session_groups = session_groups ::: List(arg)), |
102 "g:" -> (arg => session_groups = session_groups ::: List(arg)), |
102 "l:" -> (arg => logic = arg), |
|
103 "o:" -> (arg => options = options + arg), |
103 "o:" -> (arg => options = options + arg), |
104 "u:" -> (arg => options = options + ("update_" + arg)), |
104 "u:" -> (arg => options = options + ("update_" + arg)), |
105 "v" -> (_ => verbose = true), |
105 "v" -> (_ => verbose = true), |
106 "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) |
106 "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) |
107 |
107 |