From fa5d9b87b0ff4145193fce84c99a4b351cb32a1f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 20 Jan 2012 23:52:13 +0000
Subject: Added documentation for "r foo" in Ltac debugger.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14931 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tactic_debug.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'proofs/tactic_debug.ml')

diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 7d7688873f..b23f361c7c 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -71,6 +71,12 @@ let rec drop_spaces inst i =
   if String.length inst > i && inst.[i] = ' ' then drop_spaces inst (i+1)
   else i
 
+let possibly_unquote s =
+  if String.length s >= 2 & s.[0] = '"' & s.[String.length s - 1] = '"' then
+    String.sub s 1 (String.length s - 2)
+  else
+    s
+
 (* (Re-)initialize debugger *)
 let db_initialize () =
   skip:=0;skipped:=0;breakpoint:=None
@@ -86,7 +92,7 @@ let run_com inst =
         if num<0 then raise (Invalid_argument "run_com");
         skip:=num;skipped:=0
       else
-        breakpoint:=Some s
+        breakpoint:=Some (possibly_unquote s)
     else
       raise (Invalid_argument "run_com")
   else
-- 
cgit v1.2.3