From 34bdae056b1ac678419cc63437f0c92ee58ef228 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 2 Apr 2003 11:04:32 +0000 Subject: [PATCH] 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. --- helm/gTopLevel/hbugs.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) 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 () = -- 2.39.2