From 5e3a56c233ad412b96ce473cf775f6b7bd9e72f7 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 Oct 2014 16:18:19 +0200
Subject: Make rint_location_in_file resilient to Cd (close 3630)

Cd can make the relative path of the opened file wrong,
and hence not available anymore when we reopen it to compute
the line number.
---
 toplevel/coqloop.ml | 26 +++++++++++++++-----------
 1 file changed, 15 insertions(+), 11 deletions(-)

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index b27f7ae31a..3f93588904 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -159,25 +159,29 @@ let print_location_in_file {outer=s;inner=fname} loc =
       if String.equal s fname then mt() else errstrm ++ str":" ++ fnl()
     in
     let (bp,ep) = Loc.unloc loc in
-    let ic = open_in fname in
-    let rec line_of_pos lin bol cnt =
-      if cnt < bp then
-        if input_char ic == '\n'
-        then line_of_pos (lin + 1) (cnt +1) (cnt+1)
-        else line_of_pos lin bol (cnt+1)
-      else (lin, bol)
-    in
+    let line_of_pos lin bol cnt =
+      try
+        let ic = open_in fname in
+        let rec line_of_pos lin bol cnt =
+          if cnt < bp then
+            if input_char ic == '\n'
+            then line_of_pos (lin + 1) (cnt +1) (cnt+1)
+            else line_of_pos lin bol (cnt+1)
+          else (lin, bol)
+        in
+        let rc = line_of_pos lin bol cnt in
+        close_in ic;
+        rc
+      with Sys_error _ -> 0, 0 in
     try
       let (line, bol) = line_of_pos 1 0 0 in
-      close_in ic;
       hov 0 (* No line break so as to follow emacs error message format *)
         (errstrm ++ str"File " ++ str ("\""^fname^"\"") ++
            str", line " ++ int line ++ str", characters " ++
            Cerrors.print_loc (Loc.make_loc (bp-bol,ep-bol))) ++ str":" ++
         fnl ()
     with e when Errors.noncritical e ->
-      (close_in ic;
-       hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ())
+       hov 1 (errstrm ++ spc() ++ str"(invalid location):") ++ fnl ()
 
 let valid_buffer_loc ib loc =
   not (Loc.is_ghost loc) &&
-- 
cgit v1.2.3