# HG changeset patch # User wenzelm # Date 1267831281 -3600 # Node ID 78224a53cf735780dea7eeb88a4981676359119c # Parent e4331b99b03fba6030b787174ca373a18967a547# Parent 88b49baba092b8d97f57da3c5f9a902b1516b079 merged diff -r e4331b99b03f -r 78224a53cf73 doc-src/System/Thy/Presentation.thy --- a/doc-src/System/Thy/Presentation.thy Fri Mar 05 14:50:37 2010 -0800 +++ b/doc-src/System/Thy/Presentation.thy Sat Mar 06 00:21:21 2010 +0100 @@ -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} diff -r e4331b99b03f -r 78224a53cf73 doc-src/System/Thy/document/Presentation.tex --- a/doc-src/System/Thy/document/Presentation.tex Fri Mar 05 14:50:37 2010 -0800 +++ b/doc-src/System/Thy/document/Presentation.tex Sat Mar 06 00:21:21 2010 +0100 @@ -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| diff -r e4331b99b03f -r 78224a53cf73 lib/Tools/browser --- a/lib/Tools/browser Fri Mar 05 14:50:37 2010 -0800 +++ b/lib/Tools/browser Sat Mar 06 00:21:21 2010 +0100 @@ -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" diff -r e4331b99b03f -r 78224a53cf73 src/HOL/Mirabelle/Tools/mirabelle.ML --- a/src/HOL/Mirabelle/Tools/mirabelle.ML Fri Mar 05 14:50:37 2010 -0800 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Sat Mar 06 00:21:21 2010 +0100 @@ -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) diff -r e4331b99b03f -r 78224a53cf73 src/HOL/Mirabelle/Tools/mirabelle_refute.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Fri Mar 05 14:50:37 2010 -0800 +++ b/src/HOL/Mirabelle/Tools/mirabelle_refute.ML Sat Mar 06 00:21:21 2010 +0100 @@ -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 diff -r e4331b99b03f -r 78224a53cf73 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri Mar 05 14:50:37 2010 -0800 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Mar 06 00:21:21 2010 +0100 @@ -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 = diff -r e4331b99b03f -r 78224a53cf73 src/HOL/Tools/ATP_Manager/atp_manager.ML --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Fri Mar 05 14:50:37 2010 -0800 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Sat Mar 06 00:21:21 2010 +0100 @@ -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)); diff -r e4331b99b03f -r 78224a53cf73 src/HOL/Tools/ATP_Manager/atp_minimal.ML --- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 05 14:50:37 2010 -0800 +++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Sat Mar 06 00:21:21 2010 +0100 @@ -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, diff -r e4331b99b03f -r 78224a53cf73 src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Fri Mar 05 14:50:37 2010 -0800 +++ b/src/Pure/Thy/present.ML Sat Mar 06 00:21:21 2010 +0100 @@ -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));