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 0d71d94e0ddb177c928aedf72a0625a1803c6f8c..b0ad35a7402b7e97a5388066526bdf6013f3148c 100644 (file)
--- 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 () =