src/Pure/proof_general.ML
changeset 15531 08c8dad8e399
parent 15472 4674102737e9
child 15570 8d8c70b41bab
     1.1 --- a/src/Pure/proof_general.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/proof_general.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -136,15 +136,15 @@
     1.4  
     1.5  fun free_or_skolem x =
     1.6    (case try Syntax.dest_skolem x of
     1.7 -    None => tagit free_tag x
     1.8 -  | Some x' => tagit skolem_tag x');
     1.9 +    NONE => tagit free_tag x
    1.10 +  | SOME x' => tagit skolem_tag x');
    1.11  
    1.12  fun var_or_skolem s =
    1.13    (case Syntax.read_var s of
    1.14      Var ((x, i), _) =>
    1.15        (case try Syntax.dest_skolem x of
    1.16 -        None => tagit var_tag s
    1.17 -      | Some x' => tagit skolem_tag (Syntax.string_of_vname (x', i)))
    1.18 +        NONE => tagit var_tag s
    1.19 +      | SOME x' => tagit skolem_tag (Syntax.string_of_vname (x', i)))
    1.20    | _ => tagit var_tag s);
    1.21  
    1.22  val proof_general_trans =
    1.23 @@ -161,8 +161,8 @@
    1.24  
    1.25  (* assembling PGIP packets *)
    1.26  
    1.27 -val pgip_refseq = ref None : string option ref
    1.28 -val pgip_refid = ref None : string option ref
    1.29 +val pgip_refseq = ref NONE : string option ref
    1.30 +val pgip_refid = ref NONE : string option ref
    1.31  
    1.32  local
    1.33      val myseq_no = ref 1;      (* PGIP packet counter *)
    1.34 @@ -370,7 +370,7 @@
    1.35  (* misc commands for ProofGeneral/isa *)
    1.36  
    1.37  fun thms_containing ss =
    1.38 -  ProofContext.print_thms_containing (ProofContext.init (the_context ())) None ss;
    1.39 +  ProofContext.print_thms_containing (ProofContext.init (the_context ())) NONE ss;
    1.40  
    1.41  val welcome = priority o Session.welcome;
    1.42  val help = welcome;
    1.43 @@ -414,14 +414,14 @@
    1.44  
    1.45  fun which_context () =
    1.46    (case Context.get_context () of
    1.47 -    Some thy => "  Using current (dynamic!) one: " ^
    1.48 -      (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
    1.49 -  | None => "");
    1.50 +    SOME thy => "  Using current (dynamic!) one: " ^
    1.51 +      (case try PureThy.get_name thy of SOME name => quote name | NONE => "<unnamed>")
    1.52 +  | NONE => "");
    1.53  
    1.54  fun try_update_thy_only file =
    1.55    ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
    1.56      let val name = thy_name file in
    1.57 -      if is_some (ThyLoad.check_file None (ThyLoad.thy_path name)) 
    1.58 +      if is_some (ThyLoad.check_file NONE (ThyLoad.thy_path name)) 
    1.59        then update_thy_only name
    1.60        else warning ("Unkown theory context of ML file." ^ which_context ())
    1.61      end) ();
    1.62 @@ -521,8 +521,8 @@
    1.63  fun nat_option r = (pgipnat,
    1.64    withdefault (fn () => string_of_int (!r)),
    1.65    (fn s => (case Syntax.read_nat s of
    1.66 -       None => error ("nat_option: illegal value " ^ s)
    1.67 -     | Some i => r := i)));
    1.68 +       NONE => error ("nat_option: illegal value " ^ s)
    1.69 +     | SOME i => r := i)));
    1.70  
    1.71  fun bool_option r = (pgipbool,
    1.72    withdefault (fn () => Bool.toString (!r)),
    1.73 @@ -547,8 +547,8 @@
    1.74  val print_depth_option = (pgipnat,
    1.75    withdefault (fn () => string_of_int (!pg_print_depth_val)),
    1.76    (fn s => (case Syntax.read_nat s of
    1.77 -       None => error ("print_depth_option: illegal value" ^ s)
    1.78 -     | Some i => pg_print_depth i)))
    1.79 +       NONE => error ("print_depth_option: illegal value" ^ s)
    1.80 +     | SOME i => pg_print_depth i)))
    1.81  end
    1.82  
    1.83  val preferences = ref 
    1.84 @@ -656,8 +656,8 @@
    1.85  		       
    1.86      fun xml_idtable ty ctx ids = 
    1.87  	let
    1.88 -            fun ctx_attr (Some c)= [("context", c)]
    1.89 -              | ctx_attr None    = []
    1.90 +            fun ctx_attr (SOME c)= [("context", c)]
    1.91 +              | ctx_attr NONE    = []
    1.92  	    fun xmlid x = XML.element "identifier" [] [XML.text x];
    1.93  	in 
    1.94  	    XML.element "idtable" (("objtype", ty)::ctx_attr ctx)
    1.95 @@ -669,7 +669,7 @@
    1.96  fun addids t = issue_pgip "addids" [] t
    1.97  fun delids t = issue_pgip "delids" [] t
    1.98  
    1.99 -fun delallids ty = setids (xml_idtable ty None [])
   1.100 +fun delallids ty = setids (xml_idtable ty NONE [])
   1.101  
   1.102  fun send_thy_idtable ctx thys = setids (xml_idtable objtype_thy ctx thys)
   1.103  fun clear_thy_idtable () = delallids objtype_thy
   1.104 @@ -688,24 +688,24 @@
   1.105  
   1.106  local
   1.107   val topthy = Toplevel.theory_of o Toplevel.get_state
   1.108 - fun pthm thy name = print_thm (get_thm thy (name, None))
   1.109 + fun pthm thy name = print_thm (get_thm thy (name, NONE))
   1.110  
   1.111   fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
   1.112  in
   1.113 -fun askids (None, Some "theory")  = send_thy_idtable None (ThyInfo.names())
   1.114 -  | askids (None, None) =  send_thy_idtable None (ThyInfo.names())
   1.115 +fun askids (NONE, SOME "theory")  = send_thy_idtable NONE (ThyInfo.names())
   1.116 +  | askids (NONE, NONE) =  send_thy_idtable NONE (ThyInfo.names())
   1.117                             (* only theories known in top context *)
   1.118 -  | askids (Some thy, Some "theory") = send_thy_idtable (Some thy) (ThyInfo.get_preds thy)
   1.119 -  | askids (Some thy, Some "theorem") = send_thm_idtable (Some thy) (ThyInfo.get_theory thy)
   1.120 -  | askids (Some thy, None) = (send_thy_idtable (Some thy) (ThyInfo.get_preds thy);
   1.121 -                               send_thm_idtable (Some thy) (ThyInfo.get_theory thy)) 
   1.122 -  | askids (_, Some ot) = error ("No objects of type "^(quote ot)^" are available here.")
   1.123 +  | askids (SOME thy, SOME "theory") = send_thy_idtable (SOME thy) (ThyInfo.get_preds thy)
   1.124 +  | askids (SOME thy, SOME "theorem") = send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)
   1.125 +  | askids (SOME thy, NONE) = (send_thy_idtable (SOME thy) (ThyInfo.get_preds thy);
   1.126 +                               send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)) 
   1.127 +  | askids (_, SOME ot) = error ("No objects of type "^(quote ot)^" are available here.")
   1.128  
   1.129  fun showid (_,        "theory", n) = 
   1.130      with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n)))
   1.131 -  | showid (Some thy, "theorem", t) = 
   1.132 +  | showid (SOME thy, "theorem", t) = 
   1.133      with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t))
   1.134 -  | showid (None,     "theorem", t) = 
   1.135 +  | showid (NONE,     "theorem", t) = 
   1.136      with_displaywrap (idvalue "theorem" t) (fn ()=>pthm (topthy()) t)
   1.137    | showid (_, ot, _) = error ("Cannot show objects of type "^ot)
   1.138  
   1.139 @@ -779,15 +779,15 @@
   1.140      (* FIXME: allow dynamic extensions to language here: we need a hook in
   1.141         outer_syntax.ML to reset this table. *)
   1.142  
   1.143 -    val keywords_classification_table = ref (None:(string Symtab.table) option)
   1.144 +    val keywords_classification_table = ref (NONE:(string Symtab.table) option)
   1.145  
   1.146      fun get_keywords_classification_table () = 
   1.147  	case (!keywords_classification_table) of
   1.148 -	    Some t => t
   1.149 -	  | None => (let
   1.150 +	    SOME t => t
   1.151 +	  | NONE => (let
   1.152  			 val tab = foldl (fn (tab,(c,_,k,_))=>Symtab.update((c,k),tab)) 
   1.153  					 (Symtab.empty,OuterSyntax.dest_parsers())
   1.154 -		     in (keywords_classification_table := Some tab; tab) end)
   1.155 +		     in (keywords_classification_table := SOME tab; tab) end)
   1.156  
   1.157  
   1.158  		    
   1.159 @@ -929,8 +929,8 @@
   1.160     let 
   1.161         val classification = Symtab.lookup (get_keywords_classification_table(),name)
   1.162     in case classification of
   1.163 -	  Some k => (xmls_of_kind k (name,toks,str))
   1.164 -	| None => (* an uncategorized keyword ignored for undo (maybe wrong) *)
   1.165 +	  SOME k => (xmls_of_kind k (name,toks,str))
   1.166 +	| NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *)
   1.167  	  (parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd");
   1.168  	   markup_text str "spuriouscmd")
   1.169     end 
   1.170 @@ -1063,13 +1063,13 @@
   1.171  	
   1.172  fun setpref name value = 
   1.173      (case assoc (allprefs(), name) of
   1.174 -	 None => warning ("Unknown pref: " ^ quote name)
   1.175 -       | Some (_, (_, _, set)) => set value);
   1.176 +	 NONE => warning ("Unknown pref: " ^ quote name)
   1.177 +       | SOME (_, (_, _, set)) => set value);
   1.178  
   1.179  fun getpref name = 
   1.180      (case assoc (allprefs(), name) of
   1.181 -	 None => warning ("Unknown pref: " ^ quote name)
   1.182 -       | Some (_, (_, (_,get), _)) => 
   1.183 +	 NONE => warning ("Unknown pref: " ^ quote name)
   1.184 +       | SOME (_, (_, (_,get), _)) => 
   1.185  	   issue_pgip "prefval" [("name", name)] (get ()));
   1.186  
   1.187  
   1.188 @@ -1116,8 +1116,8 @@
   1.189  
   1.190    fun xmlattr attr attrs = 
   1.191        (case xmlattro attr attrs of 
   1.192 -	   Some value => value 
   1.193 -	 | None => raise PGIP ("Missing attribute: " ^ attr))
   1.194 +	   SOME value => value 
   1.195 +	 | NONE => raise PGIP ("Missing attribute: " ^ attr))
   1.196  
   1.197    val thyname_attro = xmlattro "thyname"
   1.198    val thyname_attr = xmlattr "thyname"
   1.199 @@ -1137,7 +1137,7 @@
   1.200    val topthy = Toplevel.theory_of o Toplevel.get_state
   1.201    val topthy_name = PureThy.get_name o topthy
   1.202  
   1.203 -  val currently_open_file = ref (None : string option)
   1.204 +  val currently_open_file = ref (NONE : string option)
   1.205  in
   1.206  
   1.207  fun process_pgip_element pgipxml = (case pgipxml of 
   1.208 @@ -1202,12 +1202,12 @@
   1.209       | "retracttheory"  => isarcmd ("kill_thy " ^ (quote (thyname_attr attrs)))
   1.210       | "loadfile"       => use_thy_or_ml_file (fileurl_of attrs)
   1.211       | "openfile"       => (inform_file_retracted (fileurl_of attrs);
   1.212 -			    currently_open_file := Some (fileurl_of attrs))
   1.213 +			    currently_open_file := SOME (fileurl_of attrs))
   1.214       | "closefile"      => (case !currently_open_file of 
   1.215 -				Some f => (inform_file_processed f;
   1.216 -					   currently_open_file := None)
   1.217 -			      | None => raise PGIP ("closefile when no file is open!"))
   1.218 -     | "abortfile"      => (currently_open_file := None) (* perhaps error for no file open *)
   1.219 +				SOME f => (inform_file_processed f;
   1.220 +					   currently_open_file := NONE)
   1.221 +			      | NONE => raise PGIP ("closefile when no file is open!"))
   1.222 +     | "abortfile"      => (currently_open_file := NONE) (* perhaps error for no file open *)
   1.223       | "changecwd"      => ThyLoad.add_path (dirname_attr attrs)
   1.224       | "systemcmd"	=> isarscript data
   1.225       (* unofficial command for debugging *)
   1.226 @@ -1215,8 +1215,8 @@
   1.227       | _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))
   1.228  
   1.229  fun process_pgip_tree xml = 
   1.230 -    (pgip_refseq := None; 
   1.231 -     pgip_refid := None;
   1.232 +    (pgip_refseq := NONE; 
   1.233 +     pgip_refid := NONE;
   1.234       (case xml of
   1.235  	  XML.Elem ("pgip", attrs, pgips) => 
   1.236  	  (let 
   1.237 @@ -1254,28 +1254,28 @@
   1.238  			handle e => raise XML_PARSE
   1.239      in
   1.240  	case pgipo of  
   1.241 -	     None  => ()
   1.242 -	   | Some (pgip,src') =>  
   1.243 -	     ((process_pgip_tree pgip); loop src') handle e => handler (e,Some src')
   1.244 -    end handle e => handler (e,Some src)  (* i.e. error in ready/XML parse *)
   1.245 +	     NONE  => ()
   1.246 +	   | SOME (pgip,src') =>  
   1.247 +	     ((process_pgip_tree pgip); loop src') handle e => handler (e,SOME src')
   1.248 +    end handle e => handler (e,SOME src)  (* i.e. error in ready/XML parse *)
   1.249  
   1.250  and handler (e,srco) = 
   1.251      case (e,srco) of
   1.252 -        (XML_PARSE,Some src) => 
   1.253 +        (XML_PARSE,SOME src) => 
   1.254  	(* (!error_fn "Invalid XML input, aborting"; ()) NB: loop OK for tty, but want exit on EOF *)
   1.255           panic "Invalid XML input, aborting"
   1.256        | (PGIP_QUIT,_) => ()
   1.257 -      | (ERROR,Some src) => loop src (* message already given *)
   1.258 -      | (Interrupt,Some src) => (!error_fn "Interrupt during PGIP processing"; loop src)
   1.259 -      | (Toplevel.UNDEF,Some src) => (error "No working context defined"; loop src) (* usually *)
   1.260 -      | (e,Some src) => (error (Toplevel.exn_message e); loop src)
   1.261 -      | (_,None) => ()
   1.262 +      | (ERROR,SOME src) => loop src (* message already given *)
   1.263 +      | (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop src)
   1.264 +      | (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop src) (* usually *)
   1.265 +      | (e,SOME src) => (error (Toplevel.exn_message e); loop src)
   1.266 +      | (_,NONE) => ()
   1.267  in
   1.268    (* NB: simple tty for now; later might read from other tty-style sources (e.g. sockets). *)
   1.269  
   1.270    val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
   1.271  
   1.272 -  val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP None Source.tty)
   1.273 +  val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
   1.274  
   1.275    val pgip_toplevel =  loop 
   1.276  end
   1.277 @@ -1388,7 +1388,7 @@
   1.278  
   1.279  fun make_elisp_commands commands kind =
   1.280    defconst kind (mapfilter 
   1.281 -		     (fn (c, _, k, _) => if k = kind then Some c else None) 
   1.282 +		     (fn (c, _, k, _) => if k = kind then SOME c else NONE) 
   1.283  		     commands);
   1.284  
   1.285  fun make_elisp_syntax (keywords, commands) =