# HG changeset patch
# User wenzelm
# Date 1184015569 -7200
# Node ID 09ccdb1b93baefe9267167d6a50ffe5843c4d88a
# Parent  57dceb84d1a085bf16acd492b9394bda73e756f7
use Position.file_of;
removed strange comments;

diff -r 57dceb84d1a0 -r 09ccdb1b93ba src/Pure/ProofGeneral/pgip_isabelle.ML
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Mon Jul 09 23:12:46 2007 +0200
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Mon Jul 09 23:12:49 2007 +0200
@@ -72,33 +72,20 @@
 end
 
 
-(* Now we have to parse strings constructed elsewhere in Isabelle, which is silly!
-   This is another case where Isabelle should use structured types
-   from the ground up to help its interfaces, instead of just plain
-   strings.
-*)
-fun unquote s = case explode s of 
-		    "\""::xs => (case (rev xs) of
-				    "\""::_ => SOME (String.substring(s,1,(String.size s) - 2))
-			         | _ => NONE)
-		  | _ => NONE
-
 fun location_of_position pos = 
     let val line = Position.line_of pos
 	val (url,descr) = 
-	    (case Position.name_of pos of
-		 NONE => (NONE,NONE)
-	       | SOME possiblyfile => 
-		 (case unquote possiblyfile of
-		      SOME fname => let val path = (Path.explode fname) in
-					case ThyLoad.check_file NONE path of
-					    SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
-					  | NONE => (NONE,SOME fname)
-				    end
-		    | _ => (NONE,SOME possiblyfile)))
-    in 
+	    (case Position.file_of pos of
+	       NONE => (NONE, NONE)
+	     | SOME fname => 
+	       let val path = Path.explode fname in
+		 case ThyLoad.check_file NONE path of
+		   SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
+		 | NONE => (NONE, SOME fname)
+	       end);
+    in
 	{ descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }
-    end 
+    end
 
 
 val [ObjTheoryBody,