merged

--- a/NEWS	Fri Apr 04 13:22:15 2014 +0200
+++ b/NEWS	Fri Apr 04 13:22:26 2014 +0200
@@ -642,6 +642,10 @@
 well-defined master directory, so an absolute symbolic path
 specification is usually required, e.g. "~~/src/HOL".
 
+* ML antiquotation @{print} inlines a function to print an arbitrary
+ML value, which is occasionally useful for diagnostic or demonstration
+purposes.
+
 
 *** System ***
 

--- a/src/Doc/IsarImplementation/ML.thy	Fri Apr 04 13:22:15 2014 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Fri Apr 04 13:22:26 2014 +0200
@@ -690,38 +690,52 @@
 text {* The ML compiler knows about the structure of values according
   to their static type, and can print them in the manner of the
   toplevel loop, although the details are non-portable.  The
-  antiquotation @{ML_antiquotation_def "make_string"} provides a
-  quasi-portable way to refer to this potential capability of the
-  underlying ML system in generic Isabelle/ML sources.  *}
+  antiquotations @{ML_antiquotation_def "make_string"} and
+  @{ML_antiquotation_def "print"} provide a quasi-portable way to
+  refer to this potential capability of the underlying ML system in
+  generic Isabelle/ML sources.
+
+  This is occasionally useful for diagnostic or demonstration
+  purposes.  Note that production-quality tools require proper
+  user-level error messages. *}
 
 text %mlantiq {*
   \begin{matharray}{rcl}
   @{ML_antiquotation_def "make_string"} & : & @{text ML_antiquotation} \\
+  @{ML_antiquotation_def "print"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
   @{rail \<open>
   @@{ML_antiquotation make_string}
+  ;
+  @@{ML_antiquotation print} @{syntax name}?
   \<close>}
 
   \begin{description}
 
   \item @{text "@{make_string}"} inlines a function to print arbitrary
-values similar to the ML toplevel.  The result is compiler dependent
-and may fall back on "?" in certain situations.
+  values similar to the ML toplevel.  The result is compiler dependent
+  and may fall back on "?" in certain situations.
+
+  \item @{text "@{print f}"} uses the ML function @{text "f: string ->
+  unit"} to output the result of @{text "@{make_string}"} above,
+  together with the source position of the antiquotation.  The default
+  output function is @{ML writeln}.
 
   \end{description}
 *}
 
-text %mlex {* The following artificial example shows how to produce
-  ad-hoc output of ML values for debugging purposes.  This should not
-  be done in production code, and not persist in regular Isabelle/ML
-  sources.  *}
+text %mlex {* The following artificial examples show how to produce
+  adhoc output of ML values for debugging purposes. *}
 
 ML {*
   val x = 42;
   val y = true;
 
   writeln (@{make_string} {x = x, y = y});
+
+  @{print} {x = x, y = y};
+  @{print tracing} {x = x, y = y};
 *}
 
 

--- a/src/HOL/Tools/ATP/atp_proof.ML	Fri Apr 04 13:22:15 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Fri Apr 04 13:22:26 2014 +0200
@@ -46,7 +46,6 @@
   val spass_input_rule : string
   val spass_pre_skolemize_rule : string
   val spass_skolemize_rule : string
-  val z3_tptp_core_rule : string
 
   val short_output : bool -> string -> string
   val string_of_atp_failure : atp_failure -> string
@@ -76,7 +75,6 @@
 val spass_input_rule = "Inp"
 val spass_pre_skolemize_rule = "__Sko0" (* arbitrary *)
 val spass_skolemize_rule = "__Sko" (* arbitrary *)
-val z3_tptp_core_rule = "__z3_tptp_core" (* arbitrary *)
 
 exception UNRECOGNIZED_ATP_PROOF of unit
 
@@ -148,10 +146,18 @@
      else ":\n" ^ s)
 
 fun extract_delimited (begin_delim, end_delim) output =
-  output |> first_field begin_delim |> the |> snd
-         |> first_field end_delim |> the |> fst
-         |> perhaps (try (first_field "\n" #> the #> snd))
-  handle Option.Option => ""
+  (case first_field begin_delim output of
+    SOME (_, tail) =>
+    (case first_field "\n" tail of
+      SOME (_, tail') =>
+      if end_delim = "" then
+        tail'
+      else
+        (case first_field end_delim tail' of
+          SOME (body, _) => body
+        | NONE => "")
+    | NONE => "")
+  | NONE => "")
 
 val tstp_important_message_delims =
   ("% SZS start RequiredInformation", "% SZS end RequiredInformation")
@@ -166,8 +172,7 @@
 
 (* Splits by the first possible of a list of delimiters. *)
 fun extract_tstplike_proof delims output =
-  (case pairself (find_first (fn s => String.isSubstring s output))
-                (ListPair.unzip delims) of
+  (case pairself (find_first (fn s => String.isSubstring s output)) (ListPair.unzip delims) of
     (SOME begin_delim, SOME end_delim) => extract_delimited (begin_delim, end_delim) output
   | _ => "")
 
@@ -179,7 +184,7 @@
 fun extract_tstplike_proof_and_outcome verbose proof_delims known_failures
                                        output =
   (case (extract_tstplike_proof proof_delims output,
-        extract_known_atp_failure known_failures output) of
+      extract_known_atp_failure known_failures output) of
     (_, SOME ProofIncomplete) => ("", NONE)
   | ("", SOME ProofMissing) => ("", NONE)
   | ("", NONE) => ("", SOME (UnknownError (short_output verbose output)))
@@ -218,9 +223,9 @@
       | skip n accum (ss as s :: ss') =
         if s = "," andalso n = 0 then
           (accum, ss)
-        else if member (op =) [")", "]", ">", "}"] s then
+        else if member (op =) [")", "]"] s then
           if n = 0 then (accum, ss) else skip (n - 1) (s :: accum) ss'
-        else if member (op =) ["(", "[", "<", "{"] s then
+        else if member (op =) ["(", "["] s then
           skip (n + 1) (s :: accum) ss'
         else
           skip n (s :: accum) ss'
@@ -240,7 +245,7 @@
   (parse_inference_source >> snd
    || scan_general_id --| skip_term >> single) x
 and parse_dependencies x =
-  (parse_dependency ::: Scan.repeat ($$ "," |-- parse_dependency) >> flat) x
+  (Scan.repeat (Scan.option ($$ ",") |-- parse_dependency) >> flat) x
 and parse_file_source x =
   (Scan.this_string "file" |-- $$ "(" |-- scan_general_id
    -- Scan.option ($$ "," |-- scan_general_id) --| $$ ")") x
@@ -277,7 +282,9 @@
        -- Scan.optional ($$ "<" |-- parse_types --| $$ ">") []
        -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
      >> ATerm) x
-and parse_term x = (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x
+and parse_term x =
+  (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg)
+   --| Scan.option parse_type_signature >> list_app) x
 and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
 
 fun parse_atom x =
@@ -316,8 +323,7 @@
    >> (fn ((q, ts), phi) => AQuant (q, map (fn ATerm ((s, []), _) => (s, NONE)) ts, phi))) x
 
 val parse_tstp_extra_arguments =
-  Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term))
-                dummy_inference
+  Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term)) dummy_inference
 
 val waldmeister_conjecture_name = "conjecture_1"
 
@@ -488,18 +494,12 @@
 
 fun core_inference inf fact = ((fact, [fact]), Unknown, dummy_phi, inf, [])
 
-(* Syntax: core(<name>,[<name>,...,<name>]). *)
-fun parse_z3_tptp_line x =
-  (scan_general_id --| $$ "," --| $$ "[" -- parse_dependencies --| $$ "]"
-   >> (fn (name, names) => (("", name :: names), Unknown, dummy_phi, z3_tptp_core_rule, []))) x
-
 (* Syntax: <name> *)
 fun parse_satallax_line x =
   (scan_general_id --| Scan.option ($$ " ") >> core_inference satallax_core_rule) x
 
 fun parse_line problem =
-  parse_tstp_line problem || parse_spass_line || parse_spass_pirate_line || parse_z3_tptp_line
-  || parse_satallax_line
+  parse_tstp_line problem || parse_spass_line || parse_spass_pirate_line || parse_satallax_line
 fun parse_proof problem =
   strip_spaces_except_between_idents
   #> raw_explode
@@ -540,13 +540,11 @@
       | map_term (AAbs (((s, ty), tm), args)) =
         AAbs (((f s, map_type ty), map_term tm), map map_term args)
 
-    fun map_formula (AQuant (q, xs, phi)) =
-        AQuant (q, map (apfst f) xs, map_formula phi)
+    fun map_formula (AQuant (q, xs, phi)) = AQuant (q, map (apfst f) xs, map_formula phi)
       | map_formula (AConn (c, phis)) = AConn (c, map map_formula phis)
       | map_formula (AAtom t) = AAtom (map_term t)
 
-    fun map_step (name, role, phi, rule, deps) =
-      (name, role, map_formula phi, rule, deps)
+    fun map_step (name, role, phi, rule, deps) = (name, role, map_formula phi, rule, deps)
   in
     map map_step
   end

--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Apr 04 13:22:15 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Apr 04 13:22:26 2014 +0200
@@ -621,7 +621,7 @@
   {exec = K (["Z3_TPTP_HOME"], ["z3_tptp"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
      "-proof -t:" ^ string_of_int (to_secs 1 timeout) ^ " -file:" ^ file_name,
-   proof_delims = [],
+   proof_delims = [("SZS status Theorem", "")],
    known_failures = known_szs_status_failures,
    prem_role = Hypothesis,
    best_slices =

--- a/src/Pure/ML/ml_antiquotations.ML	Fri Apr 04 13:22:15 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Fri Apr 04 13:22:26 2014 +0200
@@ -8,12 +8,7 @@
 struct
 
 val _ = Theory.setup
- (ML_Antiquotation.inline @{binding assert}
-    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
-
-  ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #>
-
-  ML_Antiquotation.value @{binding option} (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
+ (ML_Antiquotation.value @{binding option} (Scan.lift (Parse.position Args.name) >> (fn (name, pos) =>
     (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
      ML_Syntax.print_string name))) #>
 
@@ -56,6 +51,30 @@
           ML_Syntax.atomic (ML_Syntax.print_term t))));
 
 
+(* ML support *)
+
+val _ = Theory.setup
+ (ML_Antiquotation.inline @{binding assert}
+    (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
+
+  ML_Antiquotation.inline @{binding make_string} (Scan.succeed ml_make_string) #>
+
+  ML_Antiquotation.declaration @{binding print}
+    (Scan.lift (Scan.optional Args.name "Output.writeln"))
+      (fn src => fn output => fn ctxt =>
+        let
+          val (_, pos) = Args.name_of_src src;
+          val (a, ctxt') = ML_Antiquotation.variant "output" ctxt;
+          val env =
+            "val " ^ a ^ ": string -> unit =\n\
+            \  (" ^ output ^ ") o (fn s => s ^ Position.here (" ^
+            ML_Syntax.print_position pos ^ "));\n";
+          val body =
+            "(fn x => (Isabelle." ^ a ^ " (" ^ ml_make_string ^ " x); x))";
+        in (K (env, body), ctxt') end));
+
+  
+
 (* type classes *)
 
 fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) =>

--- a/src/Pure/PIDE/document.scala	Fri Apr 04 13:22:15 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Apr 04 13:22:26 2014 +0200
@@ -187,7 +187,7 @@
         }
       }
 
-      private val block_size = 1024
+      private val block_size = 256
     }
 
     final class Commands private(val commands: Linear_Set[Command])