X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Fast.ml;h=76b0ff35ed836b1c492c3e79aba1799a834fc763;hb=deb7edaccefe379139818e8b241844b9a0571651;hp=a8a5248721d5f80cb712f1b971842d1a64867b5b;hpb=dbfe6294c7bba85785a0571691d2553364409e25;p=goals.git

diff --git a/src/ast.ml b/src/ast.ml
index a8a5248..76b0ff3 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -58,7 +58,7 @@ and func = param_decl list * returning * code
 and tactic = param_decl list * code
 and param_decl = id
 and id = string
-and code = substs
+and code = substs * bool
 and returning = RetExpr | RetStrings | RetString
 and substs = subst list
 and subst =
@@ -162,20 +162,24 @@ and string_goal () (name, (param_decls, patterns, exprs, code)) =
     (String.concat ", " (List.map (string_param_decl ()) param_decls))
     (String.concat ", " (List.map (string_pattern ()) patterns))
     (String.concat ", " (List.map (string_expr ()) exprs))
-    (match code with None -> "" | Some code -> " = { ... }")
+    (match code with None -> ""
+                   | Some (code, false) -> " = { ... }"
+                   | Some (code, true) -> " = @{ ... }")
 
-and string_func () (name, (param_decls, returning, code)) =
-  sprintf "function%s returning %s (%s) = { ... }"
+and string_func () (name, (param_decls, returning, (code, quiet))) =
+  sprintf "function%s returning %s (%s) = %s{ ... }"
     (match name with None -> "" | Some name -> " " ^ name)
     (match returning with RetExpr -> "expression"
                         | RetString -> "string"
                         | RetStrings -> "strings")
     (String.concat ", " (List.map (string_param_decl ()) param_decls))
+    (if quiet then "@" else "")
 
-and string_tactic () (name, (param_decls, code)) =
-  sprintf "tactic%s (%s) = { ... }"
+and string_tactic () (name, (param_decls, (code, quiet))) =
+  sprintf "tactic%s (%s) = %s{ ... }"
     (match name with None -> "" | Some name -> " " ^ name)
     (String.concat ", " (List.map (string_param_decl ()) param_decls))
+    (if quiet then "@" else "")
 
 and string_param_decl () name = name