--- a/doc-src/System/Thy/Presentation.thy Fri Mar 05 15:25:59 2010 -0800
+++ b/doc-src/System/Thy/Presentation.thy Fri Mar 05 15:27:47 2010 -0800
@@ -183,14 +183,19 @@
Usage: browser [OPTIONS] [GRAPHFILE]
Options are:
+ -b Admin/build only
-c cleanup -- remove GRAPHFILE after use
-o FILE output to FILE (ps, eps, pdf)
\end{ttbox}
When no filename is specified, the browser automatically changes to
the directory @{setting ISABELLE_BROWSER_INFO}.
- \medskip The @{verbatim "-c"} option causes the input file to be
- removed after use.
+ \medskip The @{verbatim "-b"} option indicates that this is for
+ administrative build only, i.e.\ no browser popup if no files are
+ given.
+
+ The @{verbatim "-c"} option causes the input file to be removed
+ after use.
The @{verbatim "-o"} option indicates batch-mode operation, with the
output written to the indicated file; note that @{verbatim pdf}
--- a/doc-src/System/Thy/document/Presentation.tex Fri Mar 05 15:25:59 2010 -0800
+++ b/doc-src/System/Thy/document/Presentation.tex Fri Mar 05 15:27:47 2010 -0800
@@ -198,14 +198,19 @@
Usage: browser [OPTIONS] [GRAPHFILE]
Options are:
+ -b Admin/build only
-c cleanup -- remove GRAPHFILE after use
-o FILE output to FILE (ps, eps, pdf)
\end{ttbox}
When no filename is specified, the browser automatically changes to
the directory \hyperlink{setting.ISABELLE-BROWSER-INFO}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}BROWSER{\isacharunderscore}INFO}}}}.
- \medskip The \verb|-c| option causes the input file to be
- removed after use.
+ \medskip The \verb|-b| option indicates that this is for
+ administrative build only, i.e.\ no browser popup if no files are
+ given.
+
+ The \verb|-c| option causes the input file to be removed
+ after use.
The \verb|-o| option indicates batch-mode operation, with the
output written to the indicated file; note that \verb|pdf|
--- a/lib/Tools/browser Fri Mar 05 15:25:59 2010 -0800
+++ b/lib/Tools/browser Fri Mar 05 15:27:47 2010 -0800
@@ -13,6 +13,7 @@
echo "Usage: isabelle $PRG [OPTIONS] [GRAPHFILE]"
echo
echo " Options are:"
+ echo " -b Admin/build only"
echo " -c cleanup -- remove GRAPHFILE after use"
echo " -o FILE output to FILE (ps, eps, pdf)"
echo
@@ -30,12 +31,16 @@
# options
+ADMIN_BUILD=""
CLEAN=""
OUTFILE=""
-while getopts "co:" OPT
+while getopts "bco:" OPT
do
case "$OPT" in
+ b)
+ ADMIN_BUILD=true
+ ;;
c)
CLEAN=true
;;
@@ -64,10 +69,7 @@
classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
-if [ -z "$GRAPHFILE" ]; then
- [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
- exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser
-else
+if [ -n "$GRAPHFILE" ]; then
PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")
if [ -n "$CLEAN" ]; then
mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
@@ -95,6 +97,11 @@
fi
rm -f "$PRIVATE_FILE"
+elif [ -z "$ADMIN_BUILD" ]; then
+ [ -d "$ISABELLE_BROWSER_INFO" ] && cd "$ISABELLE_BROWSER_INFO"
+ exec "$ISABELLE_TOOL" java GraphBrowser.GraphBrowser
+else
+ RC=0
fi
exit "$RC"
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Mar 05 15:25:59 2010 -0800
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Mar 05 15:27:47 2010 -0800
@@ -27,7 +27,6 @@
unit
(*utility functions*)
- val goal_thm_of : Proof.state -> thm
val can_apply : Time.time -> (Proof.context -> int -> tactic) ->
Proof.state -> bool
val theorems_in_proof_term : thm -> thm list
@@ -155,11 +154,9 @@
(* Mirabelle utility functions *)
-val goal_thm_of = #goal o Proof.raw_goal (* FIXME ?? *)
-
fun can_apply time tac st =
let
- val {context = ctxt, facts, goal} = Proof.raw_goal st (* FIXME ?? *)
+ val {context = ctxt, facts, goal} = Proof.goal st
val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
in
(case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of
@@ -201,7 +198,7 @@
NONE => []
| SOME st =>
if not (Toplevel.is_proof st) then []
- else theorems_in_proof_term (goal_thm_of (Toplevel.proof_of st)))
+ else theorems_in_proof_term (#goal (Proof.goal (Toplevel.proof_of st))))
fun get_setting settings (key, default) =
the_default default (AList.lookup (op =) settings key)
--- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Fri Mar 05 15:25:59 2010 -0800
+++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Fri Mar 05 15:27:47 2010 -0800
@@ -10,8 +10,8 @@
fun refute_action args timeout {pre=st, ...} =
let
val subgoal = 1
- val thy = Proof.theory_of st
- val thm = goal_thm_of st
+ val thy = Proof.theory_of st
+ val thm = #goal (Proof.raw_goal st)
val refute = Refute.refute_goal thy args thm
val _ = TimeLimit.timeLimit timeout refute subgoal
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 05 15:25:59 2010 -0800
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 05 15:27:47 2010 -0800
@@ -307,7 +307,7 @@
fun run_sh prover hard_timeout timeout dir st =
let
- val {context = ctxt, facts, goal} = Proof.raw_goal st (* FIXME ?? *)
+ val {context = ctxt, facts, goal} = Proof.goal st
val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d | _ => I)
val ctxt' =
ctxt
@@ -434,39 +434,39 @@
end
fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
- let val goal = Thm.major_prem_of (#goal (Proof.raw_goal pre)) (* FIXME ?? *) in
- if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
- then () else
- let
- val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option)
- val minimize = AList.defined (op =) args minimizeK
- val metis_ft = AList.defined (op =) args metis_ftK
-
- fun apply_metis m1 m2 =
- if metis_ft
- then
- if not (Mirabelle.catch_result metis_tag false
- (run_metis false m1 name (these (!named_thms))) id st)
+ let val goal = Thm.major_prem_of (#goal (Proof.goal pre)) in
+ if can Logic.dest_conjunction goal orelse can Logic.dest_equals goal
+ then () else
+ let
+ val named_thms = Unsynchronized.ref (NONE : (string * thm list) list option)
+ val minimize = AList.defined (op =) args minimizeK
+ val metis_ft = AList.defined (op =) args metis_ftK
+
+ fun apply_metis m1 m2 =
+ if metis_ft
then
+ if not (Mirabelle.catch_result metis_tag false
+ (run_metis false m1 name (these (!named_thms))) id st)
+ then
+ (Mirabelle.catch_result metis_tag false
+ (run_metis true m2 name (these (!named_thms))) id st; ())
+ else ()
+ else
(Mirabelle.catch_result metis_tag false
- (run_metis true m2 name (these (!named_thms))) id st; ())
- else ()
- else
- (Mirabelle.catch_result metis_tag false
- (run_metis false m1 name (these (!named_thms))) id st; ())
- in
- change_data id (set_mini minimize);
- Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st;
- if is_some (!named_thms)
- then
- (apply_metis Unminimized UnminimizedFT;
- if minimize andalso not (null (these (!named_thms)))
+ (run_metis false m1 name (these (!named_thms))) id st; ())
+ in
+ change_data id (set_mini minimize);
+ Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st;
+ if is_some (!named_thms)
then
- (Mirabelle.catch minimize_tag (run_minimize args named_thms) id st;
- apply_metis Minimized MinimizedFT)
- else ())
- else ()
- end
+ (apply_metis Unminimized UnminimizedFT;
+ if minimize andalso not (null (these (!named_thms)))
+ then
+ (Mirabelle.catch minimize_tag (run_minimize args named_thms) id st;
+ apply_metis Minimized MinimizedFT)
+ else ())
+ else ()
+ end
end
fun invoke args =
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 05 15:25:59 2010 -0800
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 05 15:27:47 2010 -0800
@@ -253,7 +253,7 @@
NONE => warning ("Unknown external prover: " ^ quote name)
| SOME prover =>
let
- val {context = ctxt, facts, goal} = Proof.raw_goal proof_state; (* FIXME Proof.goal *)
+ val {context = ctxt, facts, goal} = Proof.goal proof_state;
val desc =
"external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 05 15:25:59 2010 -0800
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 05 15:27:47 2010 -0800
@@ -117,7 +117,7 @@
val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
val axclauses = Res_Axioms.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
- val {context = ctxt, facts, goal} = Proof.raw_goal state (* FIXME ?? *)
+ val {context = ctxt, facts, goal} = Proof.goal state
val problem =
{with_full_types = ! ATP_Manager.full_types,
subgoal = subgoalno,
--- a/src/Pure/Thy/present.ML Fri Mar 05 15:25:59 2010 -0800
+++ b/src/Pure/Thy/present.ML Fri Mar 05 15:27:47 2010 -0800
@@ -402,6 +402,7 @@
if length path > 1 then update_index parent_html_prefix name else ();
(case readme of NONE => () | SOME path => File.copy path html_prefix);
write_graph sorted_graph (Path.append html_prefix graph_path);
+ File.isabelle_tool "browser" "-b";
File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
(HTML.applet_pages name (Url.File index_path, name));