# HG changeset patch # User wenzelm # Date 1373742161 -7200 # Node ID 0589394aaaa5d78ed2b98677fb7efa6c2fd0b7d1 # Parent 1501ebe39711e7d4976d92dedff0a5c546931fc2# Parent ebdbd5c79a1396a935edeadb1456dd6b6e135e75 merged diff -r 1501ebe39711 -r 0589394aaaa5 NEWS --- 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. diff -r 1501ebe39711 -r 0589394aaaa5 etc/components --- 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 diff -r 1501ebe39711 -r 0589394aaaa5 src/HOL/HOL.thy --- 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 *} diff -r 1501ebe39711 -r 0589394aaaa5 src/HOL/Metis.thy --- 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 diff -r 1501ebe39711 -r 0589394aaaa5 src/HOL/Mutabelle/MutabelleExtra.thy --- 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", diff -r 1501ebe39711 -r 0589394aaaa5 src/HOL/Mutabelle/lib/Tools/mutabelle --- 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" diff -r 1501ebe39711 -r 0589394aaaa5 src/HOL/Mutabelle/mutabelle_extra.ML --- 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) diff -r 1501ebe39711 -r 0589394aaaa5 src/HOL/Nitpick.thy --- 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'}), diff -r 1501ebe39711 -r 0589394aaaa5 src/HOL/Sledgehammer.thy --- 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 diff -r 1501ebe39711 -r 0589394aaaa5 src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r 1501ebe39711 -r 0589394aaaa5 src/HOL/Tools/Nitpick/nitpick_isar.ML --- 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; diff -r 1501ebe39711 -r 0589394aaaa5 src/HOL/Tools/Predicate_Compile/etc/settings --- 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" - diff -r 1501ebe39711 -r 0589394aaaa5 src/HOL/Tools/Predicate_Compile/lib/scripts/swipl_version --- 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 diff -r 1501ebe39711 -r 0589394aaaa5 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML --- 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; diff -r 1501ebe39711 -r 0589394aaaa5 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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 diff -r 1501ebe39711 -r 0589394aaaa5 src/HOL/Tools/etc/options --- /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" + diff -r 1501ebe39711 -r 0589394aaaa5 src/HOL/Tools/try0.ML --- 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; diff -r 1501ebe39711 -r 0589394aaaa5 src/Pure/Isar/proof.ML --- 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 ""]; diff -r 1501ebe39711 -r 0589394aaaa5 src/Pure/PIDE/command.ML --- 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 diff -r 1501ebe39711 -r 0589394aaaa5 src/Pure/PIDE/command.scala --- 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) } diff -r 1501ebe39711 -r 0589394aaaa5 src/Pure/PIDE/markup.ML --- 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 *) diff -r 1501ebe39711 -r 0589394aaaa5 src/Pure/PIDE/markup.scala --- 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 */ diff -r 1501ebe39711 -r 0589394aaaa5 src/Pure/PIDE/markup_tree.scala --- 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 = diff -r 1501ebe39711 -r 0589394aaaa5 src/Pure/PIDE/protocol.scala --- 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 diff -r 1501ebe39711 -r 0589394aaaa5 src/Pure/System/session.scala --- 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 => diff -r 1501ebe39711 -r 0589394aaaa5 src/Pure/Tools/proof_general.ML --- 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") diff -r 1501ebe39711 -r 0589394aaaa5 src/Tools/jEdit/etc/options --- 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" diff -r 1501ebe39711 -r 0589394aaaa5 src/Tools/jEdit/src/rendering.scala --- 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 || diff -r 1501ebe39711 -r 0589394aaaa5 src/Tools/quickcheck.ML --- 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; diff -r 1501ebe39711 -r 0589394aaaa5 src/Tools/solve_direct.ML --- 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; diff -r 1501ebe39711 -r 0589394aaaa5 src/Tools/try.ML --- 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;