Update PGIP packet handling, fixing unique session identifier.
authoraspinall
Wed Jul 13 20:07:01 2005 +0200 (2005-07-13)
changeset 16821ba1f6aba44ed
parent 16820 5c9d597e4cb9
child 16822 7fa91e6176ed
Update PGIP packet handling, fixing unique session identifier.
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Wed Jul 13 20:02:54 2005 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Wed Jul 13 20:07:01 2005 +0200
     1.3 @@ -161,30 +161,39 @@
     1.4  
     1.5  (* assembling PGIP packets *)
     1.6  
     1.7 +val pgip_refid  = ref NONE: string option ref;  
     1.8  val pgip_refseq = ref NONE: string option ref;
     1.9 -val pgip_refid = ref NONE: string option ref;
    1.10  
    1.11  local
    1.12 -  val pgip_class  = "pg";
    1.13 -  val pgip_origin = "Isabelle/Isar";
    1.14 -  val pgip_id =
    1.15 -    getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^ Time.toString (Time.now ());
    1.16 -    (* FIXME da: PPID is empty for me: any way to get process ID? *)
    1.17 -    (* FIXME mak: consider using Path.pack (Path.base (Path.unpack (getenv "ISABELLE_TMP"))),
    1.18 -       which includes USER already; note that pgip_id above is determined at compile time! *)
    1.19 +  val pgip_class  = "pg"
    1.20 +  val pgip_tag = "Isabelle/Isar"
    1.21 +  val pgip_id = ref ""
    1.22 +  val pgip_seq = ref 0
    1.23 +  fun pgip_serial () = inc pgip_seq
    1.24  
    1.25    fun assemble_pgips pgips =
    1.26      XML.element
    1.27        "pgip"
    1.28 -      ([("class",  pgip_class),
    1.29 -        ("origin", pgip_origin),
    1.30 -        ("id",     pgip_id)] @
    1.31 -       if_none (Option.map (single o (pair "refseq")) (! pgip_refseq)) [] @
    1.32 -       if_none (Option.map (single o (pair "refid")) (! pgip_refid)) [] @
    1.33 -       [("seq",  string_of_int (Library.serial ()))])
    1.34 +      ([("tag",    pgip_tag),
    1.35 +        ("class",  pgip_class),
    1.36 +        ("id",     !pgip_id)] @
    1.37 +       if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @
    1.38 +       (* destid=refid since Isabelle only communicates back to sender,
    1.39 +          so we may omit refid from attributes.
    1.40 +       if_none (Option.map (single o (pair "refid"))  (! pgip_refid)) [] @
    1.41 +       *)
    1.42 +       if_none (Option.map (single o (pair "refseq")) (! pgip_refseq)) [])
    1.43        pgips;
    1.44 +
    1.45  in
    1.46  
    1.47 +fun init_pgip_session_id () = 
    1.48 +    pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
    1.49 +               getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
    1.50 +						       
    1.51 +
    1.52 +fun matching_pgip_id id = (id = !pgip_id)
    1.53 +
    1.54  fun decorated_output bg en prfx =
    1.55    writeln_default o enclose bg en o prefix_lines prfx;
    1.56  
    1.57 @@ -1284,26 +1293,32 @@
    1.58       | _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))
    1.59  
    1.60  fun process_pgip_tree xml =
    1.61 -    (pgip_refseq := NONE;
    1.62 -     pgip_refid := NONE;
    1.63 +    (pgip_refid := NONE;
    1.64 +     pgip_refseq := NONE;
    1.65       (case xml of
    1.66            XML.Elem ("pgip", attrs, pgips) =>
    1.67            (let
    1.68                 val class = xmlattr "class" attrs
    1.69 -               val _ = (pgip_refseq := xmlattro "seq" attrs;
    1.70 -                        pgip_refid :=  xmlattro "id" attrs)
    1.71 +	       val dest  = xmlattro "destid" attrs
    1.72 +               val _ = (pgip_refid :=  xmlattro "id" attrs;
    1.73 +			pgip_refseq := xmlattro "seq" attrs)
    1.74             in
    1.75 -               if (class = "pa") then
    1.76 -                   List.app process_pgip_element pgips
    1.77 -               else
    1.78 -                   raise PGIP "PGIP packet for me should have class=\"pa\""
    1.79 +	       (* We respond to broadcast messages to provers, or 
    1.80 +                  messages intended uniquely for us.  Silently ignore rest. *)
    1.81 +               case dest of
    1.82 +		   NONE => if (class = "pa") then
    1.83 +			       (List.app process_pgip_element pgips; true)
    1.84 +			   else false
    1.85 +		 | SOME id => if (matching_pgip_id id) then
    1.86 +				  (List.app process_pgip_element pgips; true)
    1.87 +			      else false
    1.88             end)
    1.89          | _ => raise PGIP "Invalid PGIP packet received")
    1.90       handle (PGIP msg) =>
    1.91              (error (msg ^ "\nPGIP error occured in XML text below:\n" ^
    1.92                      (XML.string_of_tree xml))))
    1.93  
    1.94 -val process_pgip = process_pgip_tree o XML.tree_of_string;
    1.95 +val process_pgip = K () o process_pgip_tree o XML.tree_of_string
    1.96  
    1.97  end
    1.98  
    1.99 @@ -1314,28 +1329,31 @@
   1.100  
   1.101  exception XML_PARSE
   1.102  
   1.103 -fun loop src : unit =
   1.104 +fun loop ready src =
   1.105      let
   1.106 -        val _ = issue_pgipe "ready" []
   1.107 +        val _ = if ready then (issue_pgipe "ready" []) else ()
   1.108          val pgipo = (Source.get_single src)
   1.109                          handle e => raise XML_PARSE
   1.110      in
   1.111          case pgipo of
   1.112               NONE  => ()
   1.113             | SOME (pgip,src') =>
   1.114 -             ((process_pgip_tree pgip); loop src') handle e => handler (e,SOME src')
   1.115 +	     let 
   1.116 +		 val ready' = (process_pgip_tree pgip) handle e => (handler (e,SOME src'); true)
   1.117 +	     in 
   1.118 +		 loop ready' src'
   1.119 +	     end 
   1.120      end handle e => handler (e,SOME src)  (* i.e. error in ready/XML parse *)
   1.121  
   1.122  and handler (e,srco) =
   1.123      case (e,srco) of
   1.124          (XML_PARSE,SOME src) =>
   1.125 -        (* (!error_fn "Invalid XML input, aborting"; ()) NB: loop OK for tty, but want exit on EOF *)
   1.126 -         panic "Invalid XML input, aborting"
   1.127 +        panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *)
   1.128        | (PGIP_QUIT,_) => ()
   1.129 -      | (ERROR,SOME src) => loop src (* message already given *)
   1.130 -      | (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop src)
   1.131 -      | (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop src) (* usually *)
   1.132 -      | (e,SOME src) => (error (Toplevel.exn_message e); loop src)
   1.133 +      | (ERROR,SOME src) => loop true src (* message already given *)
   1.134 +      | (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop true src)
   1.135 +      | (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop true src) (* usually *)
   1.136 +      | (e,SOME src) => (error (Toplevel.exn_message e); loop true src)
   1.137        | (_,NONE) => ()
   1.138  in
   1.139    (* NB: simple tty for now; later might read from other tty-style sources (e.g. sockets). *)
   1.140 @@ -1344,7 +1362,7 @@
   1.141  
   1.142    val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
   1.143  
   1.144 -  val pgip_toplevel =  loop
   1.145 +  val pgip_toplevel =  loop true
   1.146  end
   1.147  
   1.148  
   1.149 @@ -1422,7 +1440,8 @@
   1.150    sync_thy_loader ();
   1.151    print_mode := proof_generalN :: (! print_mode \ proof_generalN);
   1.152    if pgip then
   1.153 -    print_mode := pgmlN :: (pgmlatomsN :: (! print_mode \ pgmlN \ pgmlatomsN))
   1.154 +      (init_pgip_session_id();
   1.155 +       print_mode := pgmlN :: (pgmlatomsN :: (! print_mode \ pgmlN \ pgmlatomsN)))
   1.156    else
   1.157      pgip_emacs_compatibility_flag := true;  (* assume this for PG <3.6 compatibility *)
   1.158    set quick_and_dirty;