use Position.file_of;
authorwenzelm
Mon Jul 09 23:12:49 2007 +0200 (2007-07-09)
changeset 2368009ccdb1b93ba
parent 23679 57dceb84d1a0
child 23681 ccf77119dd4d
use Position.file_of;
removed strange comments;
src/Pure/ProofGeneral/pgip_isabelle.ML
     1.1 --- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Mon Jul 09 23:12:46 2007 +0200
     1.2 +++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Mon Jul 09 23:12:49 2007 +0200
     1.3 @@ -72,33 +72,20 @@
     1.4  end
     1.5  
     1.6  
     1.7 -(* Now we have to parse strings constructed elsewhere in Isabelle, which is silly!
     1.8 -   This is another case where Isabelle should use structured types
     1.9 -   from the ground up to help its interfaces, instead of just plain
    1.10 -   strings.
    1.11 -*)
    1.12 -fun unquote s = case explode s of 
    1.13 -		    "\""::xs => (case (rev xs) of
    1.14 -				    "\""::_ => SOME (String.substring(s,1,(String.size s) - 2))
    1.15 -			         | _ => NONE)
    1.16 -		  | _ => NONE
    1.17 -
    1.18  fun location_of_position pos = 
    1.19      let val line = Position.line_of pos
    1.20  	val (url,descr) = 
    1.21 -	    (case Position.name_of pos of
    1.22 -		 NONE => (NONE,NONE)
    1.23 -	       | SOME possiblyfile => 
    1.24 -		 (case unquote possiblyfile of
    1.25 -		      SOME fname => let val path = (Path.explode fname) in
    1.26 -					case ThyLoad.check_file NONE path of
    1.27 -					    SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
    1.28 -					  | NONE => (NONE,SOME fname)
    1.29 -				    end
    1.30 -		    | _ => (NONE,SOME possiblyfile)))
    1.31 -    in 
    1.32 +	    (case Position.file_of pos of
    1.33 +	       NONE => (NONE, NONE)
    1.34 +	     | SOME fname => 
    1.35 +	       let val path = Path.explode fname in
    1.36 +		 case ThyLoad.check_file NONE path of
    1.37 +		   SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
    1.38 +		 | NONE => (NONE, SOME fname)
    1.39 +	       end);
    1.40 +    in
    1.41  	{ descr=descr, url=url, line=line, column=NONE, char=NONE, length=NONE }
    1.42 -    end 
    1.43 +    end
    1.44  
    1.45  
    1.46  val [ObjTheoryBody,