From f264827750988795bd85d0eb6a7d3ecf236d224e Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 10 Feb 2005 15:45:40 +0000 Subject: [PATCH] bugfix: method 'advance' now took in input concrete syntax since atm pretty printing is not the inverse operation of parsing --- helm/matita/matitaScript.ml | 2 +- helm/matita/matitaScript.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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 -- 2.39.2