# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1250803851 -7200
# Node ID d69214e47ef9d4d13b11143e63c4f7f5fea43401
# Parent  74f0a06f751fcf665898cb0f89d88566f863ebc6
added an experimental antiquotation to replace eventually ML_response_fake

diff -r 74f0a06f751f -r d69214e47ef9 ProgTutorial/Base.thy
--- a/ProgTutorial/Base.thy	Thu Aug 20 22:30:20 2009 +0200
+++ b/ProgTutorial/Base.thy	Thu Aug 20 23:30:51 2009 +0200
@@ -5,6 +5,13 @@
   "antiquote_setup.ML"
 begin
 
+(* rebinding of writeln and tracing so that it can *)
+(* be compared in intiquotations                   *)
+ML {* 
+fun writeln s = (Output.writeln s; s)
+fun tracing s = (Output.tracing s; s)
+*}
+
 (* re-definition of various ML antiquotations    *)
 (* to have a special tag for text enclosed in ML *)
 
diff -r 74f0a06f751f -r d69214e47ef9 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Thu Aug 20 22:30:20 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Thu Aug 20 23:30:51 2009 +0200
@@ -115,7 +115,7 @@
   code. This can be done in a ``quick-and-dirty'' fashion using the function
   @{ML_ind  "writeln"}. For example
 
-  @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
+  @{ML_response_eq [display,gray] "writeln \"any string\"" "\"any string\"" with "(op =)"}
 
   will print out @{text [quotes] "any string"} inside the response buffer of
   Isabelle.  This function expects a string as argument. If you develop under
@@ -123,7 +123,7 @@
   for converting values into strings, namely the function 
   @{ML_ind  makestring in PolyML}:
 
-  @{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""} 
+  @{ML_response_eq [display,gray] "writeln (PolyML.makestring 1)" "\"1\"" with "(op =)"} 
 
   However, @{ML makestring in PolyML} only works if the type of what
   is converted is monomorphic and not a function.
@@ -134,7 +134,7 @@
   function @{ML_ind  tracing} is more appropriate. This function writes all
   output into a separate tracing buffer. For example:
 
-  @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
+  @{ML_response_eq [display,gray] "tracing \"foo\"" "\"foo\"" with "(op =)"}
 
   It is also possible to redirect the ``channel'' where the string @{text
   "foo"} is printed to a separate file, e.g., to prevent ProofGeneral from
@@ -210,7 +210,7 @@
 
   @{ML_response_fake [display,gray]
   "string_of_term @{context} @{term \"1::nat\"}"
-  "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
+  "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""} 
 
   This produces a string corrsponding to the term @{term [show_types] "1::nat"} with some
   additional information encoded in it. The string can be properly printed by
diff -r 74f0a06f751f -r d69214e47ef9 ProgTutorial/antiquote_setup.ML
--- a/ProgTutorial/antiquote_setup.ML	Thu Aug 20 22:30:20 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Thu Aug 20 23:30:51 2009 +0200
@@ -87,6 +87,7 @@
 
 val single_arg = Scan.lift (Args.name)
 val two_args   = Scan.lift (Args.name -- Args.name)
+val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with"  |-- Args.name))
 
 val _ = ThyOutput.antiquotation "ML" parser_ml output_ml
 val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind
@@ -98,6 +99,19 @@
 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake
 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both
 
+(* FIXME: experimental *)
+fun ml_eq (lhs, pat, eq) =
+  implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"] 
+
+fun output_response_eq {context = ctxt, ...} ((lhs, pat), eq) = 
+    (case eq of 
+       NONE => eval_fn ctxt (ml_pat (lhs, pat))
+     | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e));
+     output ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
+
+val _ = ThyOutput.antiquotation "ML_response_eq" test output_response_eq
+
+(* checks whether a file exists in the Isabelle distribution *)
 fun href_link txt =
 let 
   val raw = Symbol.encode_raw
@@ -106,13 +120,11 @@
  implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"]
 end 
 
-(* checks whether a file exists in the Isabelle distribution *)
 fun check_file_exists _ txt =
   (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 
    then output [href_link txt]
    else error (implode ["Source file ", quote txt, " does not exist."]))
 
-
 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists
 
 
diff -r 74f0a06f751f -r d69214e47ef9 progtutorial.pdf
Binary file progtutorial.pdf has changed