From 939d3c17b57049422f584857725e04ff9cbbf2e4 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 31 Aug 2009 20:03:29 +0000
Subject: Prevent reporting column number back to Isabelle process as not
 reliable; extra work needed on both sides. See
 http://proofgeneral.inf.ed.ac.uk/trac/ticket/277

---
 isar/isar.el | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/isar/isar.el b/isar/isar.el
index b3b03121..305680ea 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -557,15 +557,17 @@ Checks the width in the `proof-goals-buffer'"
    "\""))
 
 (defun isar-positions-of (buffer span)
-  (let (line column)
+  (let (line)
     (if span
 	(save-excursion
 	  (set-buffer (span-buffer span))
 	  (goto-char (span-start span))
 	  (skip-chars-forward " \t\n")
 	  ;; NB: position is relative to display (narrowing, etc)
-	  (setq line (line-number-at-pos (point)))
-	  (setq column (current-column))))
+	  ;; defer column: too tricky for now (Isabelle symbols 
+	  ;; vs displayed chars, etc)
+	  ; (setq column (current-column))
+	  (setq line (line-number-at-pos (point)))))
     (concat
      "("
      (proof-splice-separator 
@@ -574,8 +576,8 @@ Checks the width in the `proof-goals-buffer'"
        (if (and buffer (buffer-file-name buffer))
 	   (format "\"file\"=%s" 
 		   (isar-string-wrapping (buffer-file-name buffer))))
-       (if line   (format "\"line\"=\"%d\"" line))
-       (if column (format "\"column\"=\"%d\"" column))))
+       (if line   (format "\"line\"=\"%d\"" line))))
+       ;(if column (format "\"column\"=\"%d\"" column))))
       ") ")))
 
 (defun isar-command-wrapping (string scriptspan)
-- 
cgit v1.2.3