# HG changeset patch
# User haftmann
# Date 1251834259 -7200
# Node ID a4a1547a6f1e99e84a1e7620d01c182e369ba950
# Parent  d2c97fc18704ebd6d6f756d925ebc3eb59a47579# Parent  522f04b719c826582b6976cc48a9aaa20663bf7a
merged

diff -r 522f04b719c8 -r a4a1547a6f1e src/HOL/Tools/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Tue Sep 01 17:02:09 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Tue Sep 01 21:44:19 2009 +0200
@@ -38,8 +38,8 @@
 
 (* Mirabelle core *)
 
-type action = Time.time -> {pre: Proof.state, post: Toplevel.state option} ->
-  string option
+type action = {pre: Proof.state, post: Toplevel.state option,
+  timeout: Time.time, log: string -> unit} -> unit
 
 structure Actions = TheoryDataFun
 (
@@ -67,33 +67,30 @@
   (* FIXME: with multithreading and parallel proofs enabled, we might need to
      encapsulate this inside a critical section *)
 
-fun capture_exns f x =
+fun log_block thy msg = log thy (msg ^ "\n------------------")
+fun log_action thy name msg = log_block thy (name ^ ": " ^ msg)
+
+fun capture_exns logf f x =
   let
     fun f' x = f x
-      handle TimeLimit.TimeOut => SOME "time out"
-           | ERROR msg => SOME ("error: " ^ msg)
-  in (case try f' x of NONE => SOME "exception" | SOME msg => msg) end
+      handle TimeLimit.TimeOut => logf "time out"
+           | ERROR msg => logf ("error: " ^ msg)
+  in (case try f' x of NONE => logf "exception" | _ => ()) end
 
-fun apply_action timeout st (name, action) =
-  Option.map (pair name) (capture_exns (action timeout) st)
+fun apply_actions thy info (pre, post, time) actions =
+  let
+    val _ = log_block thy info
+    fun apply (name, action) =
+      let val st = {pre=pre, post=post, timeout=time, log=log_action thy name}
+      in capture_exns (log_action thy name) action st end
+  in List.app apply actions end
 
 fun in_range _ _ NONE = true
   | in_range l r (SOME i) = (l <= i andalso (r < 0 orelse i <= r))
 
 fun only_within_range thy pos f x =
   let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
-  in if in_range l r (Position.line_of pos) then f x else [] end
-
-fun pretty_print pos name msgs =
-  let
-    val str0 = string_of_int o the_default 0
-    val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
-    val head = "at " ^ loc ^ " (" ^ name ^ "):"
-
-    fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg])
-  in
-    Pretty.string_of (Pretty.big_list head (map pretty_msg msgs))
-  end
+  in if in_range l r (Position.line_of pos) then f x else () end
 
 in
 
@@ -102,18 +99,20 @@
     val thy = Proof.theory_of pre
     val pos = Toplevel.pos_of tr
     val name = Toplevel.name_of tr
-    val timeout = Time.fromSeconds (Config.get_thy thy timeout)
-    val st = {pre=pre, post=post}
+    val st = (pre, post, Time.fromSeconds (Config.get_thy thy timeout))
+
+    val str0 = string_of_int o the_default 0
+    val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
+    val info = "\n\nat " ^ loc ^ " (" ^ name ^ "):"
   in
     Actions.get thy
     |> Symtab.dest
-    |> only_within_range thy pos (map_filter (apply_action timeout st))
-    |> (fn [] => () | msgs => log thy (pretty_print pos name msgs))
+    |> only_within_range thy pos (apply_actions thy info st)
   end
 
 end
 
-val blacklist = ["disable_pr", "enable_pr", "done", "."]
+val blacklist = ["disable_pr", "enable_pr", "done", ".", "txt"]
 
 fun step_hook tr pre post =
  (* FIXME: might require wrapping into "interruptible" *)
@@ -128,12 +127,12 @@
 
 val goal_thm_of = snd o snd o Proof.get_goal
 
-fun can_apply timeout tac st =
+fun can_apply time tac st =
   let
     val (ctxt, (facts, goal)) = Proof.get_goal st
     val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
   in
-    (case TimeLimit.timeLimit timeout (Seq.pull o full_tac) goal of
+    (case TimeLimit.timeLimit time (Seq.pull o full_tac) goal of
       SOME (thm, _) => true
     | NONE => false)
   end
diff -r 522f04b719c8 -r a4a1547a6f1e src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML	Tue Sep 01 17:02:09 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_arith.ML	Tue Sep 01 21:44:19 2009 +0200
@@ -5,10 +5,10 @@
 structure Mirabelle_Arith : MIRABELLE_ACTION =
 struct
 
-fun arith_action timeout {pre=st, ...} =
-  if Mirabelle.can_apply timeout Arith_Data.arith_tac st
-  then SOME "succeeded"
-  else NONE
+fun arith_action {pre, timeout, log, ...} =
+  if Mirabelle.can_apply timeout Arith_Data.arith_tac pre
+  then log "succeeded"
+  else ()
 
 fun invoke _ = Mirabelle.register ("arith", arith_action)
 
diff -r 522f04b719c8 -r a4a1547a6f1e src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML	Tue Sep 01 17:02:09 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_metis.ML	Tue Sep 01 21:44:19 2009 +0200
@@ -5,18 +5,19 @@
 structure Mirabelle_Metis : MIRABELLE_ACTION =
 struct
 
-fun metis_action timeout {pre, post} =
+fun metis_action {pre, post, timeout, log} =
   let
     val thms = Mirabelle.theorems_of_sucessful_proof post
     val names = map Thm.get_name thms
+    val add_info = if null names then I else suffix (":\n" ^ commas names)
 
     val facts = Facts.props (ProofContext.facts_of (Proof.context_of pre))
 
     fun metis ctxt = MetisTools.metis_tac ctxt (thms @ facts)
   in
     (if Mirabelle.can_apply timeout metis pre then "succeeded" else "failed")
-    |> suffix (" (" ^ commas names ^ ")")
-    |> SOME
+    |> add_info
+    |> log
   end
 
 fun invoke _ = Mirabelle.register ("metis", metis_action)
diff -r 522f04b719c8 -r a4a1547a6f1e src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Sep 01 17:02:09 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Sep 01 21:44:19 2009 +0200
@@ -29,7 +29,7 @@
 val keepK = "keep"
 val metisK = "metis"
 
-fun sledgehammer_action args timeout {pre=st, ...} =
+fun sledgehammer_action args {pre=st, timeout, log, ...} =
   let
     val prover_name =
       AList.lookup (op =) args proverK
@@ -56,25 +56,28 @@
           TimeLimit.timeLimit timeout atp (Proof.get_goal st)
       in (success, message, SOME thm_names) end
       handle ResHolClause.TOO_TRIVIAL => (true, "trivial", SOME [])
-           | ERROR msg => (false, "error: " ^ msg, NONE)
     val (success, message, thm_names) = safe init done sh
       (AList.lookup (op =) args keepK)
+    val _ =
+      if success then log (quote prover_name ^ " succeeded:\n" ^ message)
+      else log (prover_name ^ " failed")
 
     (* try metis *)
     fun get_thms ctxt = maps (thms_of_name ctxt)
     fun metis thms ctxt = MetisTools.metis_tac ctxt thms
-    fun apply_metis thms = "\nApplying metis with these theorems: " ^
-     (if Mirabelle.can_apply timeout (metis thms) st
-      then "success"
-      else "failure")
-    val msg = if not (AList.defined (op =) args metisK) then ""
-      else (apply_metis (get_thms (Proof.context_of st) (these thm_names))
-        handle ERROR m => "\nException: " ^ m)
-  in
-    if success
-    then SOME ("success (" ^ prover_name ^ ": " ^ message ^ ")" ^ msg)
-    else NONE
-  end
+    fun log_metis s =
+      log ("applying metis: " ^ s)
+    fun apply_metis thms =
+      if Mirabelle.can_apply timeout (metis thms) st
+      then "succeeded" else "failed"
+    val _ =
+      if not (AList.defined (op =) args metisK) then ()
+      else
+        these thm_names
+        |> get_thms (Proof.context_of st)
+        |> apply_metis
+        |> log_metis
+  in () end
 
 fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args)
 
diff -r 522f04b719c8 -r a4a1547a6f1e src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Tue Sep 01 17:02:09 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Tue Sep 01 21:44:19 2009 +0200
@@ -120,7 +120,6 @@
 foreach $name (@action_names) {
   print LOG_FILE "  $name\n";
 }
-print LOG_FILE "\n\n";
 close(LOG_FILE);
 
 my $r = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
diff -r 522f04b719c8 -r a4a1547a6f1e src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Tue Sep 01 17:02:09 2009 +0200
+++ b/src/Pure/Isar/isar_document.ML	Tue Sep 01 21:44:19 2009 +0200
@@ -15,7 +15,7 @@
   val edit_document: document_id -> document_id -> (command_id * command_id option) list -> unit
 end;
 
-structure IsarDocument: ISAR_DOCUMENT =
+structure Isar_Document: ISAR_DOCUMENT =
 struct
 
 (* unique identifiers *)
diff -r 522f04b719c8 -r a4a1547a6f1e src/Pure/Isar/isar_document.scala
--- a/src/Pure/Isar/isar_document.scala	Tue Sep 01 17:02:09 2009 +0200
+++ b/src/Pure/Isar/isar_document.scala	Tue Sep 01 21:44:19 2009 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 
-object IsarDocument
+object Isar_Document
 {
   /* unique identifiers */
 
@@ -17,9 +17,9 @@
 }
 
 
-trait IsarDocument extends Isabelle_Process
+trait Isar_Document extends Isabelle_Process
 {
-  import IsarDocument._
+  import Isar_Document._
 
 
   /* commands */
diff -r 522f04b719c8 -r a4a1547a6f1e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Sep 01 17:02:09 2009 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Sep 01 21:44:19 2009 +0200
@@ -30,7 +30,7 @@
 
 val _ =
   OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
-    (ThyHeader.args >> (Toplevel.print oo IsarCmd.init_theory));
+    (Thy_Header.args >> (Toplevel.print oo IsarCmd.init_theory));
 
 val _ =
   OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
diff -r 522f04b719c8 -r a4a1547a6f1e src/Pure/ProofGeneral/pgip_parser.ML
--- a/src/Pure/ProofGeneral/pgip_parser.ML	Tue Sep 01 17:02:09 2009 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Tue Sep 01 21:44:19 2009 +0200
@@ -20,7 +20,7 @@
 fun badcmd text = [D.Badcmd {text = text}];
 
 fun thy_begin text =
-  (case try (ThyHeader.read Position.none) (Source.of_string text) of
+  (case try (Thy_Header.read Position.none) (Source.of_string text) of
     NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
   | SOME (name, imports, _) =>
        D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
diff -r 522f04b719c8 -r a4a1547a6f1e src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Tue Sep 01 17:02:09 2009 +0200
+++ b/src/Pure/Thy/thy_header.ML	Tue Sep 01 21:44:19 2009 +0200
@@ -11,7 +11,7 @@
   val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
 end;
 
-structure ThyHeader: THY_HEADER =
+structure Thy_Header: THY_HEADER =
 struct
 
 structure T = OuterLex;
diff -r 522f04b719c8 -r a4a1547a6f1e src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Tue Sep 01 17:02:09 2009 +0200
+++ b/src/Pure/Thy/thy_header.scala	Tue Sep 01 21:44:19 2009 +0200
@@ -7,7 +7,7 @@
 package isabelle
 
 
-object ThyHeader
+object Thy_Header
 {
   val HEADER = "header"
   val THEORY = "theory"
diff -r 522f04b719c8 -r a4a1547a6f1e src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Tue Sep 01 17:02:09 2009 +0200
+++ b/src/Pure/Thy/thy_load.ML	Tue Sep 01 21:44:19 2009 +0200
@@ -109,7 +109,7 @@
     val master as (path, _) = check_thy dir name;
     val text = explode (File.read path);
     val (name', imports, uses) =
-      ThyHeader.read (Path.position path) (Source.of_list_limited 8000 text);
+      Thy_Header.read (Path.position path) (Source.of_list_limited 8000 text);
     val _ = check_name name name';
     val uses = map (Path.explode o #1) uses;
   in {master = master, text = text, imports = imports, uses = uses} end;