From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 10 Feb 2005 15:45:40 +0000 (+0000)
Subject: bugfix: method 'advance' now took in input concrete syntax since atm
X-Git-Tag: before_svn_merge~11
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f264827750988795bd85d0eb6a7d3ecf236d224e;p=helm.git

bugfix: method 'advance' now took in input concrete syntax since atm
pretty printing is not the inverse operation of parsing
---

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index acb73fb54..69334355f 100644
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -114,7 +114,7 @@ class script ~(interpreter:MatitaTypes.interpreter) () =
       gui#main#showScriptMenuItem#set_active true
 
     method advance tactical =
-      let text = "\n" ^ TacticAstPp.pp_tactical tactical in
+      let text = "\n" ^ tactical in
       buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) text;
       let res = self#_forward () in
       if not (fst res) then begin
diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli
index cdcb5a544..b1d32eb99 100644
--- a/helm/matita/matitaScript.mli
+++ b/helm/matita/matitaScript.mli
@@ -38,7 +38,7 @@ class type script =
       (** adds a tactical at current script execution point and execute it. Used
       * when the user uses buttons or console instead of directly editing the
       * script *)
-    method advance: DisambiguateTypes.tactical -> MatitaTypes.command_outcome
+    method advance: string -> MatitaTypes.command_outcome
   end
 
 val script: interpreter:MatitaTypes.interpreter -> script