From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 2 Apr 2003 11:04:32 +0000 (+0000)
Subject: We have a big architectural problem here: the Hbugs hints when applied
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=34bdae056b1ac678419cc63437f0c92ee58ef228;p=helm.git

We have a big architectural problem here: the Hbugs hints when applied
may have an argument which is a term (now in textual form). Depending on the
current parser in use, the syntax for the textual form must be TeX or
ASCII art. Which one is the right one? The current momentary patch activates
the TeX syntax.
---

diff --git a/helm/gTopLevel/hbugs.ml b/helm/gTopLevel/hbugs.ml
index 0d71d94e0..b0ad35a74 100644
--- a/helm/gTopLevel/hbugs.ml
+++ b/helm/gTopLevel/hbugs.ml
@@ -100,7 +100,14 @@ module Make (Tactics: InvokeTactics.Tactics) : HbugsActions =
       | Use_split_Luke -> Tactics.split ()
       | Use_left_Luke -> Tactics.left ()
       | Use_right_Luke -> Tactics.right ()
-      | Use_apply_Luke term -> Tactics.apply ~term ()
+      | Use_apply_Luke term ->
+         (* CSC: patch momentanea: la stringa deve essere nel formato *)
+         (* CSC: corretto (ovvero quotata se e' TeX ;-(((             *)
+         let term =
+          let term' = String.sub term 4 (String.length term - 4) in
+           "$" ^ Str.global_replace (Str.regexp "_") "\\_" term' ^ "$"
+         in
+          Tactics.apply ~term ()
       | Hints _ -> assert false
 
     let rec enable () =