--- a/NEWS Sat Jul 13 17:53:58 2013 +0200
+++ b/NEWS Sat Jul 13 21:02:41 2013 +0200
@@ -43,6 +43,16 @@
*** Prover IDE -- Isabelle/Scala/jEdit ***
+* Strictly monotonic document update, without premature cancelation of
+running transactions that are still needed: avoid reset/restart of
+such command executions while editing.
+
+* Support for asynchronous print functions, as overlay to existing
+document content.
+
+* Support for automatic tools in HOL, which try to prove or disprove
+toplevel theorem statements.
+
* Dockable window "Documentation" provides access to Isabelle
documentation.
--- a/etc/components Sat Jul 13 17:53:58 2013 +0200
+++ b/etc/components Sat Jul 13 21:02:41 2013 +0200
@@ -5,8 +5,8 @@
src/HOL/Mirabelle
src/HOL/Mutabelle
src/HOL/Library/Sum_of_Squares
+src/HOL/Tools
src/HOL/Tools/ATP
-src/HOL/Tools/Predicate_Compile
src/HOL/Tools/Sledgehammer/MaSh
src/HOL/Tools/SMT
src/HOL/TPTP
--- a/src/HOL/HOL.thy Sat Jul 13 17:53:58 2013 +0200
+++ b/src/HOL/HOL.thy Sat Jul 13 21:02:41 2013 +0200
@@ -37,8 +37,6 @@
setup {*
Intuitionistic.method_setup @{binding iprover}
- #> Quickcheck.setup
- #> Solve_Direct.setup
#> Subtyping.setup
#> Case_Product.setup
*}
--- a/src/HOL/Metis.thy Sat Jul 13 17:53:58 2013 +0200
+++ b/src/HOL/Metis.thy Sat Jul 13 21:02:41 2013 +0200
@@ -56,6 +56,5 @@
subsection {* Try0 *}
ML_file "Tools/try0.ML"
-setup {* Try0.setup *}
end
--- a/src/HOL/Mutabelle/MutabelleExtra.thy Sat Jul 13 17:53:58 2013 +0200
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy Sat Jul 13 21:02:41 2013 +0200
@@ -26,7 +26,6 @@
nitpick_params [timeout = 5, sat_solver = MiniSat, no_overlord, verbose, card = 1-5, iter = 1,2,4,8,12]
refute_params [maxtime = 10, minsize = 1, maxsize = 5, satsolver = jerusat]
*)
-ML {* Try.auto_time_limit := 10.0 *}
ML {* val mtds = [
MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.finite_types false) "random",
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle Sat Jul 13 17:53:58 2013 +0200
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle Sat Jul 13 21:02:41 2013 +0200
@@ -133,7 +133,8 @@
# execution
-"$ISABELLE_PROCESS" -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -q "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
+"$ISABELLE_PROCESS" -o auto_time_limit=10.0 \
+ -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -q "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1
[ $? -ne 0 ] && echo "isabelle processing of mutabelle failed"
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Sat Jul 13 17:53:58 2013 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sat Jul 13 21:02:41 2013 +0200
@@ -120,7 +120,7 @@
| SOME _ => (GenuineCex, Quickcheck.timings_of result)
end) ()
handle TimeLimit.TimeOut =>
- (Timeout, [("timelimit", Real.floor (!Try.auto_time_limit))])
+ (Timeout, [("timelimit", Real.floor (Options.default_real @{option auto_time_limit}))])
fun quickcheck_mtd change_options quickcheck_generator =
("quickcheck_" ^ quickcheck_generator, invoke_quickcheck change_options)
--- a/src/HOL/Nitpick.thy Sat Jul 13 17:53:58 2013 +0200
+++ b/src/HOL/Nitpick.thy Sat Jul 13 21:02:41 2013 +0200
@@ -214,7 +214,6 @@
ML_file "Tools/Nitpick/nitpick_tests.ML"
setup {*
- Nitpick_Isar.setup #>
Nitpick_HOL.register_ersatz_global
[(@{const_name card}, @{const_name card'}),
(@{const_name setsum}, @{const_name setsum'}),
--- a/src/HOL/Sledgehammer.thy Sat Jul 13 17:53:58 2013 +0200
+++ b/src/HOL/Sledgehammer.thy Sat Jul 13 21:02:41 2013 +0200
@@ -11,7 +11,6 @@
keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
begin
-
ML_file "Tools/Sledgehammer/async_manager.ML"
ML_file "Tools/Sledgehammer/sledgehammer_util.ML"
ML_file "Tools/Sledgehammer/sledgehammer_annotate.ML"
@@ -31,6 +30,4 @@
ML_file "Tools/Sledgehammer/sledgehammer_run.ML"
ML_file "Tools/Sledgehammer/sledgehammer_isar.ML"
-setup {* Sledgehammer_Isar.setup *}
-
end
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Jul 13 17:53:58 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Jul 13 21:02:41 2013 +0200
@@ -240,8 +240,7 @@
fun pprint print =
if mode = Auto_Try then
Unsynchronized.change state_ref o Proof.goal_message o K
- o Pretty.chunks o cons (Pretty.str "") o single
- o Pretty.mark Markup.intensify
+ o Pretty.mark Markup.information
else
print o Pretty.string_of
val pprint_a = pprint Output.urgent_message
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Jul 13 17:53:58 2013 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sat Jul 13 21:02:41 2013 +0200
@@ -12,9 +12,7 @@
val nitpickN : string
val nitpick_paramsN : string
- val auto : bool Unsynchronized.ref
val default_params : theory -> (string * string) list -> params
- val setup : theory -> theory
end;
structure Nitpick_Isar : NITPICK_ISAR =
@@ -29,16 +27,14 @@
val nitpickN = "nitpick"
val nitpick_paramsN = "nitpick_params"
-val auto = Unsynchronized.ref false
-
(* Maximum number of scopes for Auto Nitpick. Be frugal since it has to share
its time slot with several other automatic tools. *)
val auto_try_max_scopes = 6
val _ =
- ProofGeneral.preference_bool ProofGeneral.category_tracing
+ ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- auto
+ @{option auto_nitpick}
"auto-nitpick"
"Run Nitpick automatically"
@@ -402,6 +398,6 @@
fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
-val setup = Try.register_tool (nitpickN, (50, auto, try_nitpick))
+val _ = Try.tool_setup (nitpickN, (50, @{option auto_nitpick}, try_nitpick))
end;
--- a/src/HOL/Tools/Predicate_Compile/etc/settings Sat Jul 13 17:53:58 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-# -*- shell-script -*- :mode=shellscript:
-
-ISABELLE_PREDICATE_COMPILE="$COMPONENT"
-
--- a/src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version Sat Jul 13 17:53:58 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Lukas Bulwahn, TU Muenchen, 2010
-#
-# Determine SWI-Prolog version
-
-if [ "$ISABELLE_SWIPL" != "" ]; then
- VERSION="$("$ISABELLE_SWIPL" --version)"
- REGEXP='^SWI-Prolog version ([0-9\.]*) for .*$'
- if [[ "$VERSION" =~ $REGEXP ]]; then
- echo -n "${BASH_REMATCH[1]}"
- else
- echo -n undefined
- fi
-fi
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Jul 13 17:53:58 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Jul 13 21:02:41 2013 +0200
@@ -8,11 +8,9 @@
sig
type params = Sledgehammer_Provers.params
- val auto : bool Unsynchronized.ref
val provers : string Unsynchronized.ref
val timeout : int Unsynchronized.ref
val default_params : Proof.context -> (string * string) list -> params
- val setup : theory -> theory
end;
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
@@ -42,12 +40,10 @@
val running_learnersN = "running_learners"
val refresh_tptpN = "refresh_tptp"
-val auto = Unsynchronized.ref false
-
val _ =
- ProofGeneral.preference_bool ProofGeneral.category_tracing
+ ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- auto
+ @{option auto_sledgehammer}
"auto-sledgehammer"
"Run Sledgehammer automatically"
@@ -497,6 +493,6 @@
(minimize_command [] i) state
end
-val setup = Try.register_tool (sledgehammerN, (40, auto, try_sledgehammer))
+val _ = Try.tool_setup (sledgehammerN, (40, @{option auto_sledgehammer}, try_sledgehammer))
end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Jul 13 17:53:58 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Jul 13 21:02:41 2013 +0200
@@ -140,9 +140,7 @@
state
|> outcome_code = someN
? Proof.goal_message (fn () =>
- [Pretty.str "",
- Pretty.mark Markup.intensify (Pretty.str (message ()))]
- |> Pretty.chunks))
+ Pretty.mark Markup.information (Pretty.str (message ()))))
end
else if blocking then
let
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/etc/options Sat Jul 13 21:02:41 2013 +0200
@@ -0,0 +1,25 @@
+(* :mode=isabelle-options: *)
+
+section {* Automatically tried tools *}
+
+public option auto_time_start : real = 1.0
+ -- "initial delay for automatically tried tools (seconds)"
+
+public option auto_time_limit : real = 2.0
+ -- "time limit for automatically tried tools (seconds > 0)"
+
+public option auto_nitpick : bool = false
+ -- "run Nitpick automatically"
+
+public option auto_sledgehammer : bool = false
+ -- "run Sledgehammer automatically"
+
+public option auto_try0 : bool = false
+ -- "try standard proof methods automatically"
+
+public option auto_quickcheck : bool = true
+ -- "run Quickcheck automatically"
+
+public option auto_solve_direct : bool = true
+ -- "run solve_direct automatically"
+
--- a/src/HOL/Tools/try0.ML Sat Jul 13 17:53:58 2013 +0200
+++ b/src/HOL/Tools/try0.ML Sat Jul 13 21:02:41 2013 +0200
@@ -8,11 +8,9 @@
sig
val try0N : string
val noneN : string
- val auto : bool Unsynchronized.ref
val try0 :
Time.time option -> string list * string list * string list * string list
-> Proof.state -> bool
- val setup : theory -> theory
end;
structure Try0 : TRY0 =
@@ -24,12 +22,10 @@
val noneN = "none"
-val auto = Unsynchronized.ref false
-
val _ =
- ProofGeneral.preference_bool ProofGeneral.category_tracing
+ ProofGeneral.preference_option ProofGeneral.category_tracing
NONE
- auto
+ @{option auto_try0}
"auto-try0"
"Try standard proof methods"
@@ -144,13 +140,12 @@
Active.sendback_markup
((if nprems_of (#goal (Proof.goal st)) = 1 then "by"
else "apply") ^ " " ^ (s |> need_parens ? enclose "(" ")")) ^
- "\n(" ^ space_implode "; " (map time_string xs) ^ ").\n"
+ "\n(" ^ space_implode "; " (map time_string xs) ^ ")."
in
(true, (s, st |> (if mode = Auto_Try then
Proof.goal_message
- (fn () => Pretty.chunks [Pretty.str "",
- Pretty.markup Markup.intensify
- [Pretty.str message]])
+ (fn () => Pretty.markup Markup.information
+ [Pretty.str message])
else
tap (fn _ => Output.urgent_message message))))
end
@@ -196,6 +191,6 @@
fun try_try0 auto =
do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])
-val setup = Try.register_tool (try0N, (30, auto, try_try0))
+val _ = Try.tool_setup (try0N, (30, @{option auto_try0}, try_try0))
end;
--- a/src/Pure/Isar/proof.ML Sat Jul 13 17:53:58 2013 +0200
+++ b/src/Pure/Isar/proof.ML Sat Jul 13 21:02:41 2013 +0200
@@ -32,6 +32,7 @@
val assert_no_chain: state -> state
val enter_forward: state -> state
val goal_message: (unit -> Pretty.T) -> state -> state
+ val pretty_goal_messages: state -> Pretty.T list
val pretty_state: int -> state -> Pretty.T list
val refine: Method.text -> state -> state Seq.seq
val refine_end: Method.text -> state -> state Seq.seq
@@ -336,6 +337,11 @@
(** pretty_state **)
+fun pretty_goal_messages state =
+ (case try find_goal state of
+ SOME (_, (_, {messages, ...})) => map (fn msg => msg ()) (rev messages)
+ | NONE => []);
+
fun pretty_facts _ _ NONE = []
| pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths, Pretty.str ""];
--- a/src/Pure/PIDE/command.ML Sat Jul 13 17:53:58 2013 +0200
+++ b/src/Pure/PIDE/command.ML Sat Jul 13 21:02:41 2013 +0200
@@ -15,8 +15,9 @@
type print
val print: bool -> string -> eval -> print list -> print list option
type print_fn = Toplevel.transition -> Toplevel.state -> unit
- val print_function: {name: string, pri: int, persistent: bool} ->
- ({command_name: string} -> print_fn option) -> unit
+ val print_function: string ->
+ ({command_name: string} ->
+ {delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option) -> unit
val no_print_function: string -> unit
type exec = eval * print list
val no_exec: exec
@@ -192,15 +193,19 @@
(* print *)
datatype print = Print of
- {name: string, pri: int, persistent: bool,
+ {name: string, delay: Time.time, pri: int, persistent: bool,
exec_id: Document_ID.exec, print_process: unit memo};
type print_fn = Toplevel.transition -> Toplevel.state -> unit;
+type print_function =
+ {command_name: string} ->
+ {delay: Time.time, pri: int, persistent: bool, print_fn: print_fn} option;
+
local
-type print_function = string * (int * bool * ({command_name: string} -> print_fn option));
-val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
+val print_functions =
+ Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
fun print_error tr e =
(Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e ()
@@ -219,9 +224,9 @@
fun print command_visible command_name eval old_prints =
let
- fun new_print (name, (pri, persistent, get_fn)) =
+ fun new_print (name, get_pr) =
let
- fun make_print strict print_fn =
+ fun make_print strict {delay, pri, persistent, print_fn} =
let
val exec_id = Document_ID.make ();
fun process () =
@@ -234,14 +239,17 @@
end;
in
Print {
- name = name, pri = pri, persistent = persistent,
+ name = name, delay = delay, pri = pri, persistent = persistent,
exec_id = exec_id, print_process = memo exec_id process}
end;
in
- (case Exn.capture (Runtime.controlled_execution get_fn) {command_name = command_name} of
+ (case Exn.capture (Runtime.controlled_execution get_pr) {command_name = command_name} of
Exn.Res NONE => NONE
- | Exn.Res (SOME print_fn) => SOME (make_print false print_fn)
- | Exn.Exn exn => SOME (make_print true (fn _ => fn _ => reraise exn)))
+ | Exn.Res (SOME pr) => SOME (make_print false pr)
+ | Exn.Exn exn =>
+ SOME (make_print true
+ {delay = Time.zeroTime, pri = 0, persistent = false,
+ print_fn = fn _ => fn _ => reraise exn}))
end;
val new_prints =
@@ -255,11 +263,11 @@
if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
end;
-fun print_function {name, pri, persistent} f =
+fun print_function name f =
Synchronized.change print_functions (fn funs =>
(if not (AList.defined (op =) funs name) then ()
else warning ("Redefining command print function: " ^ quote name);
- AList.update (op =) (name, (pri, persistent, f)) funs));
+ AList.update (op =) (name, f) funs));
fun no_print_function name =
Synchronized.change print_functions (filter_out (equal name o #1));
@@ -267,15 +275,17 @@
end;
val _ =
- print_function {name = "print_state", pri = 0, persistent = true}
- (fn {command_name} => SOME (fn tr => fn st' =>
- let
- val is_init = Keyword.is_theory_begin command_name;
- val is_proof = Keyword.is_proof command_name;
- val do_print =
- not is_init andalso
- (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
- in if do_print then Toplevel.print_state false st' else () end));
+ print_function "print_state"
+ (fn {command_name} =>
+ SOME {delay = Time.zeroTime, pri = 0, persistent = true,
+ print_fn = fn tr => fn st' =>
+ let
+ val is_init = Keyword.is_theory_begin command_name;
+ val is_proof = Keyword.is_proof command_name;
+ val do_print =
+ not is_init andalso
+ (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
+ in if do_print then Toplevel.print_state false st' else () end});
(* combined execution *)
@@ -290,10 +300,18 @@
local
-fun run_print execution_id (Print {name, pri, print_process, ...}) =
- (if Multithreading.enabled () then
- memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true}
- else memo_exec) execution_id print_process;
+fun run_print execution_id (Print {name, delay, pri, print_process, ...}) =
+ if Multithreading.enabled () then
+ let
+ val group = Future.worker_subgroup ();
+ fun fork () =
+ memo_fork {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
+ execution_id print_process;
+ in
+ if delay = Time.zeroTime then fork ()
+ else ignore (Event_Timer.request (Time.+ (Time.now (), delay)) fork)
+ end
+ else memo_exec execution_id print_process;
in
--- a/src/Pure/PIDE/command.scala Sat Jul 13 17:53:58 2013 +0200
+++ b/src/Pure/PIDE/command.scala Sat Jul 13 21:02:41 2013 +0200
@@ -130,7 +130,10 @@
}
def ++ (other: State): State =
- copy(results = results ++ other.results) // FIXME merge more content!?
+ copy(
+ status = other.status ::: status,
+ results = results ++ other.results,
+ markup = markup ++ other.markup)
}
--- a/src/Pure/PIDE/markup.ML Sat Jul 13 17:53:58 2013 +0200
+++ b/src/Pure/PIDE/markup.ML Sat Jul 13 21:02:41 2013 +0200
@@ -133,6 +133,7 @@
val no_reportN: string val no_report: T
val badN: string val bad: T
val intensifyN: string val intensify: T
+ val informationN: string val information: T
val browserN: string
val graphviewN: string
val sendbackN: string
@@ -440,6 +441,7 @@
val (badN, bad) = markup_elem "bad";
val (intensifyN, intensify) = markup_elem "intensify";
+val (informationN, information) = markup_elem "information";
(* active areas *)
--- a/src/Pure/PIDE/markup.scala Sat Jul 13 17:53:58 2013 +0200
+++ b/src/Pure/PIDE/markup.scala Sat Jul 13 21:02:41 2013 +0200
@@ -293,6 +293,7 @@
val BAD = "bad"
val INTENSIFY = "intensify"
+ val INFORMATION = "information"
/* active areas */
--- a/src/Pure/PIDE/markup_tree.scala Sat Jul 13 17:53:58 2013 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Sat Jul 13 21:02:41 2013 +0200
@@ -184,6 +184,10 @@
}
}
+ def ++ (other: Markup_Tree): Markup_Tree =
+ (this /: other.branches)({ case (tree, (range, entry)) =>
+ ((tree ++ entry.subtree) /: entry.markup)({ case (t, elem) => t + Text.Info(range, elem) }) })
+
def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): XML.Body =
{
def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
--- a/src/Pure/PIDE/protocol.scala Sat Jul 13 17:53:58 2013 +0200
+++ b/src/Pure/PIDE/protocol.scala Sat Jul 13 21:02:41 2013 +0200
@@ -205,15 +205,18 @@
case _ => false
}
- def is_state(msg: XML.Tree): Boolean =
+ def is_writeln_markup(msg: XML.Tree, name: String): Boolean =
msg match {
case XML.Elem(Markup(Markup.WRITELN, _),
- List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+ List(XML.Elem(markup, _))) => markup.name == name
case XML.Elem(Markup(Markup.WRITELN_MESSAGE, _),
- List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+ List(XML.Elem(markup, _))) => markup.name == name
case _ => false
}
+ def is_state(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.STATE)
+ def is_information(msg: XML.Tree): Boolean = is_writeln_markup(msg, Markup.INFORMATION)
+
def is_warning(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Markup.WARNING, _), _) => true
--- a/src/Pure/System/session.scala Sat Jul 13 17:53:58 2013 +0200
+++ b/src/Pure/System/session.scala Sat Jul 13 21:02:41 2013 +0200
@@ -335,6 +335,23 @@
}
+ /* raw edits */
+
+ def handle_raw_edits(edits: List[Document.Edit_Text])
+ //{{{
+ {
+ prover.get.discontinue_execution()
+
+ val previous = global_state().history.tip.version
+ val version = Future.promise[Document.Version]
+ val change = global_state >>> (_.continue_history(previous, edits, version))
+
+ raw_edits.event(Session.Raw_Edits(edits))
+ change_parser ! Text_Edits(previous, edits, version)
+ }
+ //}}}
+
+
/* resulting changes */
def handle_change(change: Change)
@@ -480,22 +497,18 @@
reply(())
case Update_Options(options) if prover.isDefined =>
- if (is_ready) prover.get.options(options)
+ if (is_ready) {
+ prover.get.options(options)
+ handle_raw_edits(Nil)
+ }
global_options.event(Session.Global_Options(options))
reply(())
case Cancel_Execution if prover.isDefined =>
prover.get.cancel_execution()
- case raw @ Session.Raw_Edits(edits) if prover.isDefined =>
- prover.get.discontinue_execution()
-
- val previous = global_state().history.tip.version
- val version = Future.promise[Document.Version]
- val change = global_state >>> (_.continue_history(previous, edits, version))
- raw_edits.event(raw)
- change_parser ! Text_Edits(previous, edits, version)
-
+ case Session.Raw_Edits(edits) if prover.isDefined =>
+ handle_raw_edits(edits)
reply(())
case Session.Dialog_Result(id, serial, result) if prover.isDefined =>
--- a/src/Pure/Tools/proof_general.ML Sat Jul 13 17:53:58 2013 +0200
+++ b/src/Pure/Tools/proof_general.ML Sat Jul 13 21:02:41 2013 +0200
@@ -230,6 +230,7 @@
else if name = Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
else if name = Markup.sendbackN then (special "W", special "X")
else if name = Markup.intensifyN then (special "0", special "1")
+ else if name = Markup.informationN then ("\n" ^ special "0", special "1")
else if name = Markup.tfreeN then (special "C", special "A")
else if name = Markup.tvarN then (special "D", special "A")
else if name = Markup.freeN then (special "E", special "A")
--- a/src/Tools/jEdit/etc/options Sat Jul 13 17:53:58 2013 +0200
+++ b/src/Tools/jEdit/etc/options Sat Jul 13 21:02:41 2013 +0200
@@ -42,10 +42,12 @@
option bullet_color : string = "000000FF"
option tooltip_color : string = "FFFFE9FF"
option writeln_color : string = "C0C0C0FF"
+option information_color : string = "C1DFEEFF"
option warning_color : string = "FF8C00FF"
option error_color : string = "B22222FF"
option error1_color : string = "B2222232"
option writeln_message_color : string = "F0F0F0FF"
+option information_message_color : string = "C1DFEE32"
option tracing_message_color : string = "F0F8FFFF"
option warning_message_color : string = "EEE8AAFF"
option error_message_color : string = "FFC1C1FF"
@@ -75,18 +77,9 @@
section "Icons"
-(* jEdit/Tango *)
-(*
-option tooltip_close_icon : string = "16x16/actions/document-close.png"
-option tooltip_detach_icon : string = "16x16/actions/window-new.png"
-option gutter_warning_icon : string = "16x16/status/dialog-information.png"
-option gutter_legacy_icon : string = "16x16/status/dialog-warning.png"
-option gutter_error_icon : string = "16x16/status/dialog-error.png"
-*)
-
-(* IntelliJ IDEA *)
option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png"
option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png"
+option gutter_information_icon : string = "idea-icons/general/balloonInformation.png"
option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png"
option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png"
option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png"
--- a/src/Tools/jEdit/src/rendering.scala Sat Jul 13 17:53:58 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Sat Jul 13 21:02:41 2013 +0200
@@ -28,10 +28,11 @@
/* message priorities */
private val writeln_pri = 1
- private val tracing_pri = 2
- private val warning_pri = 3
- private val legacy_pri = 4
- private val error_pri = 5
+ private val information_pri = 2
+ private val tracing_pri = 3
+ private val warning_pri = 4
+ private val legacy_pri = 5
+ private val error_pri = 6
private val message_pri = Map(
Markup.WRITELN -> writeln_pri, Markup.WRITELN_MESSAGE -> writeln_pri,
@@ -123,10 +124,12 @@
val bullet_color = color_value("bullet_color")
val tooltip_color = color_value("tooltip_color")
val writeln_color = color_value("writeln_color")
+ val information_color = color_value("information_color")
val warning_color = color_value("warning_color")
val error_color = color_value("error_color")
val error1_color = color_value("error1_color")
val writeln_message_color = color_value("writeln_message_color")
+ val information_message_color = color_value("information_message_color")
val tracing_message_color = color_value("tracing_message_color")
val warning_message_color = color_value("warning_message_color")
val error_message_color = color_value("error_message_color")
@@ -383,15 +386,21 @@
private lazy val gutter_icons = Map(
+ Rendering.information_pri -> Rendering.load_icon(options.string("gutter_information_icon")),
Rendering.warning_pri -> Rendering.load_icon(options.string("gutter_warning_icon")),
Rendering.legacy_pri -> Rendering.load_icon(options.string("gutter_legacy_icon")),
Rendering.error_pri -> Rendering.load_icon(options.string("gutter_error_icon")))
+ private val gutter_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+
def gutter_message(range: Text.Range): Option[Icon] =
{
val results =
- snapshot.cumulate_markup[Int](range, 0, Some(Set(Markup.WARNING, Markup.ERROR)), _ =>
+ snapshot.cumulate_markup[Int](range, 0, Some(gutter_elements), _ =>
{
+ case (pri, Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _),
+ List(XML.Elem(Markup(Markup.INFORMATION, _), _))))) =>
+ pri max Rendering.information_pri
case (pri, Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body))) =>
body match {
case List(XML.Elem(Markup(Markup.LEGACY, _), _)) =>
@@ -408,19 +417,23 @@
private val squiggly_colors = Map(
Rendering.writeln_pri -> writeln_color,
+ Rendering.information_pri -> information_color,
Rendering.warning_pri -> warning_color,
Rendering.error_pri -> error_color)
+ private val squiggly_elements = Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)
+
def squiggly_underline(range: Text.Range): Stream[Text.Info[Color]] =
{
val results =
- snapshot.cumulate_markup[Int](range, 0,
- Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR)), _ =>
+ snapshot.cumulate_markup[Int](range, 0, Some(squiggly_elements), _ =>
{
- case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
+ case (pri, Text.Info(_, msg @ XML.Elem(Markup(name, _), _)))
if name == Markup.WRITELN ||
name == Markup.WARNING ||
- name == Markup.ERROR => pri max Rendering.message_pri(name)
+ name == Markup.ERROR =>
+ if (Protocol.is_information(msg)) pri max Rendering.information_pri
+ else pri max Rendering.message_pri(name)
})
for {
Text.Info(r, pri) <- results
@@ -429,20 +442,24 @@
}
- private val messages_include =
- Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.ERROR_MESSAGE)
-
private val message_colors = Map(
Rendering.writeln_pri -> writeln_message_color,
+ Rendering.information_pri -> information_message_color,
Rendering.tracing_pri -> tracing_message_color,
Rendering.warning_pri -> warning_message_color,
Rendering.error_pri -> error_message_color)
+ private val line_background_elements =
+ Set(Markup.WRITELN_MESSAGE, Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE,
+ Markup.ERROR_MESSAGE, Markup.INFORMATION)
+
def line_background(range: Text.Range): Option[(Color, Boolean)] =
{
val results =
- snapshot.cumulate_markup[Int](range, 0, Some(messages_include), _ =>
+ snapshot.cumulate_markup[Int](range, 0, Some(line_background_elements), _ =>
{
+ case (pri, Text.Info(_, XML.Elem(Markup(Markup.INFORMATION, _), _))) =>
+ pri max Rendering.information_pri
case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
if name == Markup.WRITELN_MESSAGE ||
name == Markup.TRACING_MESSAGE ||
--- a/src/Tools/quickcheck.ML Sat Jul 13 17:53:58 2013 +0200
+++ b/src/Tools/quickcheck.ML Sat Jul 13 21:02:41 2013 +0200
@@ -10,9 +10,7 @@
val genuineN: string
val noneN: string
val unknownN: string
- val setup: theory -> theory
(*configuration*)
- val auto: bool Unsynchronized.ref
val batch_tester : string Config.T
val size : int Config.T
val iterations : int Config.T
@@ -94,12 +92,10 @@
(* preferences *)
-val auto = Unsynchronized.ref false;
-
val _ =
- ProofGeneral.preference_bool ProofGeneral.category_tracing
- (SOME "true")
- auto
+ ProofGeneral.preference_option ProofGeneral.category_tracing
+ NONE
+ @{option auto_quickcheck}
"auto-quickcheck"
"Run Quickcheck automatically";
@@ -557,8 +553,7 @@
(genuineN,
state
|> (if auto then
- Proof.goal_message (K (Pretty.chunks [Pretty.str "",
- Pretty.mark Markup.intensify msg]))
+ Proof.goal_message (K (Pretty.mark Markup.information msg))
else
tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
else
@@ -567,8 +562,7 @@
end
|> `(fn (outcome_code, _) => outcome_code = genuineN);
-val setup = Try.register_tool (quickcheckN, (20, auto, try_quickcheck));
+val _ = Try.tool_setup (quickcheckN, (20, @{option auto_quickcheck}, try_quickcheck));
end;
-val auto_quickcheck = Quickcheck.auto;
--- a/src/Tools/solve_direct.ML Sat Jul 13 17:53:58 2013 +0200
+++ b/src/Tools/solve_direct.ML Sat Jul 13 21:02:41 2013 +0200
@@ -14,10 +14,8 @@
val someN: string
val noneN: string
val unknownN: string
- val auto: bool Unsynchronized.ref
val max_solutions: int Unsynchronized.ref
val solve_direct: Proof.state -> bool * (string * Proof.state)
- val setup: theory -> theory
end;
structure Solve_Direct: SOLVE_DIRECT =
@@ -33,13 +31,12 @@
(* preferences *)
-val auto = Unsynchronized.ref false;
val max_solutions = Unsynchronized.ref 5;
val _ =
- ProofGeneral.preference_bool ProofGeneral.category_tracing
- (SOME "true")
- auto
+ ProofGeneral.preference_option ProofGeneral.category_tracing
+ NONE
+ @{option auto_solve_direct}
"auto-solve-direct"
("Run " ^ quote solve_directN ^ " automatically");
@@ -88,8 +85,7 @@
(if mode = Auto_Try then
Proof.goal_message
(fn () =>
- Pretty.chunks
- [Pretty.str "", Pretty.markup Markup.intensify (message results)])
+ Pretty.markup Markup.information (message results))
else
tap (fn _ =>
Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))
@@ -117,6 +113,6 @@
fun try_solve_direct auto = do_solve_direct (if auto then Auto_Try else Try)
-val setup = Try.register_tool (solve_directN, (10, auto, try_solve_direct));
+val _ = Try.tool_setup (solve_directN, (10, @{option auto_solve_direct}, try_solve_direct));
end;
--- a/src/Tools/try.ML Sat Jul 13 17:53:58 2013 +0200
+++ b/src/Tools/try.ML Sat Jul 13 21:02:41 2013 +0200
@@ -7,37 +7,32 @@
signature TRY =
sig
type tool =
- string * (int * bool Unsynchronized.ref
- * (bool -> Proof.state -> bool * (string * Proof.state)))
+ string * (int * string * (bool -> Proof.state -> bool * (string * Proof.state)))
val tryN : string
- val auto_time_limit: real Unsynchronized.ref
val serial_commas : string -> string list -> string list
val subgoal_count : Proof.state -> int
- val register_tool : tool -> theory -> theory
val get_tools : theory -> tool list
val try_tools : Proof.state -> (string * string) option
+ val tool_setup : tool -> unit
end;
structure Try : TRY =
struct
type tool =
- string * (int * bool Unsynchronized.ref
- * (bool -> Proof.state -> bool * (string * Proof.state)))
+ string * (int * string * (bool -> Proof.state -> bool * (string * Proof.state)))
val tryN = "try"
(* preferences *)
-val auto_time_limit = Unsynchronized.ref 4.0
-
val _ =
- ProofGeneral.preference_real ProofGeneral.category_tracing
- NONE
- auto_time_limit
+ ProofGeneral.preference_option ProofGeneral.category_tracing
+ (SOME "4.0")
+ @{option auto_time_limit}
"auto-try-time-limit"
"Time limit for automatically tried tools (in seconds)"
@@ -70,6 +65,7 @@
val register_tool = Data.map o Ord_List.insert tool_ord
+
(* try command *)
fun try_tools state =
@@ -94,11 +90,11 @@
(Scan.succeed (Toplevel.unknown_proof o Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
-(* automatic try *)
+(* automatic try (TTY) *)
fun auto_try state =
get_tools (Proof.theory_of state)
- |> map_filter (fn (_, (_, auto, tool)) => if !auto then SOME tool else NONE)
+ |> map_filter (fn (_, (_, auto, tool)) => if Options.default_bool auto then SOME tool else NONE)
|> Par_List.get_some (fn tool =>
case try (tool true) state of
SOME (true, (_, state)) => SOME state
@@ -106,10 +102,46 @@
|> the_default state
val _ = Context.>> (Specification.add_theorem_hook (fn interact => fn state =>
- if interact andalso not (!Toplevel.quiet) andalso !auto_time_limit > 0.0 then
- TimeLimit.timeLimit (seconds (!auto_time_limit)) auto_try state
- handle TimeLimit.TimeOut => state
- else
- state))
+ let
+ val auto_time_limit = Options.default_real @{option auto_time_limit}
+ in
+ if interact andalso not (!Toplevel.quiet) andalso auto_time_limit > 0.0 then
+ TimeLimit.timeLimit (seconds auto_time_limit) auto_try state
+ handle TimeLimit.TimeOut => state
+ else
+ state
+ end))
+
+
+(* asynchronous print function (PIDE) *)
+
+fun print_function ((name, (weight, auto, tool)): tool) =
+ Command.print_function name
+ (fn {command_name} =>
+ if Keyword.is_theory_goal command_name andalso Options.default_bool auto then
+ SOME
+ {delay = seconds (Options.default_real @{option auto_time_start}),
+ pri = ~ weight,
+ persistent = true,
+ print_fn = fn _ => fn st =>
+ let
+ val state = Toplevel.proof_of st
+ |> Proof.map_context (Context_Position.set_visible false)
+ val auto_time_limit = Options.default_real @{option auto_time_limit}
+ in
+ if auto_time_limit > 0.0 then
+ (case TimeLimit.timeLimit (seconds auto_time_limit) (fn () => tool true state) () of
+ (true, (_, state')) =>
+ List.app Pretty.writeln (Proof.pretty_goal_messages state')
+ | _ => ())
+ else ()
+ end handle exn => if Exn.is_interrupt exn then reraise exn else ()}
+ else NONE)
+
+
+(* hybrid tool setup *)
+
+fun tool_setup tool =
+ (Context.>> (Context.map_theory (register_tool tool)); print_function tool)
end;