Quote arguments in PGIP exceptions. Tune comment.
authoraspinall
Sun Dec 31 15:34:21 2006 +0100 (2006-12-31)
changeset 21973e7c9b0d3ce82
parent 21972 1b68312c4cf0
child 21974 c4e4d34fbc60
Quote arguments in PGIP exceptions. Tune comment.
src/Pure/ProofGeneral/pgip_types.ML
     1.1 --- a/src/Pure/ProofGeneral/pgip_types.ML	Sun Dec 31 14:55:35 2006 +0100
     1.2 +++ b/src/Pure/ProofGeneral/pgip_types.ML	Sun Dec 31 15:34:21 2006 +0100
     1.3 @@ -122,7 +122,7 @@
     1.4  fun get_attr attr attrs =
     1.5      (case get_attr_opt attr attrs of
     1.6           SOME value => value
     1.7 -       | NONE => raise PGIP ("Missing attribute: " ^ attr))
     1.8 +       | NONE => raise PGIP ("Missing attribute: " ^ quote attr))
     1.9  
    1.10  fun get_attr_dflt attr dflt attrs = the_default dflt (get_attr_opt attr attrs)
    1.11  
    1.12 @@ -188,7 +188,7 @@
    1.13      (case s of 
    1.14  	 "false" => false 
    1.15         | "true" => true 
    1.16 -       | _ => raise PGIP ("Invalid boolean value: "^s))
    1.17 +       | _ => raise PGIP ("Invalid boolean value: " ^ quote s))
    1.18  
    1.19  local
    1.20      fun int_in_range (NONE,NONE) _ = true
    1.21 @@ -199,21 +199,21 @@
    1.22  fun read_pgipint range s =
    1.23      (case Syntax.read_int s of 
    1.24  	 SOME i => if int_in_range range i then i
    1.25 -		   else raise PGIP ("Out of range integer value: "^s)
    1.26 -       | NONE => raise PGIP ("Invalid integer value: "^s))
    1.27 +		   else raise PGIP ("Out of range integer value: " ^ quote s)
    1.28 +       | NONE => raise PGIP ("Invalid integer value: " ^ quote s))
    1.29  end;
    1.30  
    1.31  fun read_pgipnat s =
    1.32      (case Syntax.read_nat s of 
    1.33  	 SOME i => i
    1.34 -       | NONE => raise PGIP ("Invalid natural number: "^s))
    1.35 +       | NONE => raise PGIP ("Invalid natural number: " ^ quote s))
    1.36  
    1.37  (* NB: we can maybe do without xml decode/encode here. *)
    1.38  fun read_pgipstring s =  (* non-empty strings, XML escapes decoded *)
    1.39      (case XML.parse_string s of
    1.40  	 SOME s => s
    1.41 -       | NONE => raise PGIP ("Expected a non-empty string: "^s))
    1.42 -    handle _ => raise PGIP ("Invalid XML string syntax: "^s)
    1.43 +       | NONE => raise PGIP ("Expected a non-empty string: " ^ quote s))
    1.44 +    handle _ => raise PGIP ("Invalid XML string syntax: " ^ quote s)
    1.45  
    1.46  val int_to_pgstring = signed_string_of_int
    1.47  
    1.48 @@ -292,13 +292,13 @@
    1.49  
    1.50  fun read_pguval Pgipnull s = 
    1.51      if s="" then Pgvalnull
    1.52 -    else raise PGIP ("Expecting empty string for null type, not: "^s)
    1.53 +    else raise PGIP ("Expecting empty string for null type, not: " ^ quote s)
    1.54    | read_pguval Pgipbool s = Pgvalbool (read_pgipbool s)
    1.55    | read_pguval (Pgipint range) s = Pgvalint (read_pgipint range s)
    1.56    | read_pguval Pgipnat s = Pgvalnat (read_pgipnat s)
    1.57    | read_pguval (Pgipconst c) s = 
    1.58      if c=s then Pgvalconst c 
    1.59 -    else raise PGIP ("Given string: "^s^" doesn't match expected string: "^c)
    1.60 +    else raise PGIP ("Given string: "^quote s^" doesn't match expected string: "^quote c)
    1.61    | read_pguval Pgipstring s = 
    1.62      if s<>"" then Pgvalstring s
    1.63      else raise PGIP ("Expecting non-empty string, empty string illegal.")
    1.64 @@ -310,7 +310,7 @@
    1.65  		       (fn ty => SOME (read_pguval ty s) handle PGIP _ => NONE)
    1.66  		       (map getty tydescs)
    1.67      in
    1.68 -	case uval of SOME pgv => pgv | NONE => raise PGIP ("Can't match string: "^s^
    1.69 +	case uval of SOME pgv => pgv | NONE => raise PGIP ("Can't match string: "^quote s^
    1.70  							   " against any allowed types.")
    1.71      end
    1.72  
    1.73 @@ -346,11 +346,11 @@
    1.74  fun pgipurl_of_string url = (* only handle file:/// or file://localhost/ *)
    1.75  	case Url.explode url of
    1.76              (Url.File path) => path
    1.77 -	  | _ => raise PGIP ("Cannot access non-local URL " ^ url)
    1.78 +	  | _ => raise PGIP ("Cannot access non-local URL " ^ quote url)
    1.79  		       
    1.80  fun pgipurl_of_path p = p
    1.81  
    1.82 -fun path_of_pgipurl p = p  (* potentially raises PGIP *)
    1.83 +fun path_of_pgipurl p = p  (* potentially raises PGIP, but not with this implementation *)
    1.84  
    1.85  fun attrs_of_pgipurl purl = 
    1.86      [("url", "file:" ^ (XML.text (File.platform_path (File.full_path purl))))]
    1.87 @@ -358,7 +358,8 @@
    1.88  val pgipurl_of_attrs = pgipurl_of_string o get_attr "url"
    1.89  
    1.90  fun pgipurl_of_url (Url.File p) = p
    1.91 -  | pgipurl_of_url url = raise PGIP ("Cannot access non-local/non-file URL " ^ (Url.implode url))
    1.92 +  | pgipurl_of_url url = 
    1.93 +    raise PGIP ("Cannot access non-local/non-file URL " ^ quote (Url.implode url))
    1.94  
    1.95  
    1.96  (** Messages and errors **)
    1.97 @@ -403,7 +404,7 @@
    1.98      fun pgipint_of_string err s = 
    1.99  	case Syntax.read_int s of 
   1.100  	    SOME i => i
   1.101 -	  | NONE => raise PGIP ("Type error in " ^ err ^ ": expected integer.")
   1.102 +	  | NONE => raise PGIP ("Type error in " ^ quote err ^ ": expected integer.")
   1.103  
   1.104    fun location_of_attrs attrs = 
   1.105        let