# HG changeset patch # User aspinall # Date 1121278021 -7200 # Node ID ba1f6aba44edbb0bee93f12484eb82cc2a683786 # Parent 5c9d597e4cb910d5398acea024451e85dacc0afe Update PGIP packet handling, fixing unique session identifier. diff -r 5c9d597e4cb9 -r ba1f6aba44ed src/Pure/proof_general.ML --- a/src/Pure/proof_general.ML Wed Jul 13 20:02:54 2005 +0200 +++ b/src/Pure/proof_general.ML Wed Jul 13 20:07:01 2005 +0200 @@ -161,30 +161,39 @@ (* assembling PGIP packets *) +val pgip_refid = ref NONE: string option ref; val pgip_refseq = ref NONE: string option ref; -val pgip_refid = ref NONE: string option ref; local - val pgip_class = "pg"; - val pgip_origin = "Isabelle/Isar"; - val pgip_id = - getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^ Time.toString (Time.now ()); - (* FIXME da: PPID is empty for me: any way to get process ID? *) - (* FIXME mak: consider using Path.pack (Path.base (Path.unpack (getenv "ISABELLE_TMP"))), - which includes USER already; note that pgip_id above is determined at compile time! *) + val pgip_class = "pg" + val pgip_tag = "Isabelle/Isar" + val pgip_id = ref "" + val pgip_seq = ref 0 + fun pgip_serial () = inc pgip_seq fun assemble_pgips pgips = XML.element "pgip" - ([("class", pgip_class), - ("origin", pgip_origin), - ("id", pgip_id)] @ - if_none (Option.map (single o (pair "refseq")) (! pgip_refseq)) [] @ - if_none (Option.map (single o (pair "refid")) (! pgip_refid)) [] @ - [("seq", string_of_int (Library.serial ()))]) + ([("tag", pgip_tag), + ("class", pgip_class), + ("id", !pgip_id)] @ + if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @ + (* destid=refid since Isabelle only communicates back to sender, + so we may omit refid from attributes. + if_none (Option.map (single o (pair "refid")) (! pgip_refid)) [] @ + *) + if_none (Option.map (single o (pair "refseq")) (! pgip_refseq)) []) pgips; + in +fun init_pgip_session_id () = + pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^ + getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ()) + + +fun matching_pgip_id id = (id = !pgip_id) + fun decorated_output bg en prfx = writeln_default o enclose bg en o prefix_lines prfx; @@ -1284,26 +1293,32 @@ | _ => raise PGIP ("Unrecognized PGIP element: " ^ elem))) fun process_pgip_tree xml = - (pgip_refseq := NONE; - pgip_refid := NONE; + (pgip_refid := NONE; + pgip_refseq := NONE; (case xml of XML.Elem ("pgip", attrs, pgips) => (let val class = xmlattr "class" attrs - val _ = (pgip_refseq := xmlattro "seq" attrs; - pgip_refid := xmlattro "id" attrs) + val dest = xmlattro "destid" attrs + val _ = (pgip_refid := xmlattro "id" attrs; + pgip_refseq := xmlattro "seq" attrs) in - if (class = "pa") then - List.app process_pgip_element pgips - else - raise PGIP "PGIP packet for me should have class=\"pa\"" + (* We respond to broadcast messages to provers, or + messages intended uniquely for us. Silently ignore rest. *) + case dest of + NONE => if (class = "pa") then + (List.app process_pgip_element pgips; true) + else false + | SOME id => if (matching_pgip_id id) then + (List.app process_pgip_element pgips; true) + else false end) | _ => raise PGIP "Invalid PGIP packet received") handle (PGIP msg) => (error (msg ^ "\nPGIP error occured in XML text below:\n" ^ (XML.string_of_tree xml)))) -val process_pgip = process_pgip_tree o XML.tree_of_string; +val process_pgip = K () o process_pgip_tree o XML.tree_of_string end @@ -1314,28 +1329,31 @@ exception XML_PARSE -fun loop src : unit = +fun loop ready src = let - val _ = issue_pgipe "ready" [] + val _ = if ready then (issue_pgipe "ready" []) else () val pgipo = (Source.get_single src) handle e => raise XML_PARSE in case pgipo of NONE => () | SOME (pgip,src') => - ((process_pgip_tree pgip); loop src') handle e => handler (e,SOME src') + let + val ready' = (process_pgip_tree pgip) handle e => (handler (e,SOME src'); true) + in + loop ready' src' + end end handle e => handler (e,SOME src) (* i.e. error in ready/XML parse *) and handler (e,srco) = case (e,srco) of (XML_PARSE,SOME src) => - (* (!error_fn "Invalid XML input, aborting"; ()) NB: loop OK for tty, but want exit on EOF *) - panic "Invalid XML input, aborting" + panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *) | (PGIP_QUIT,_) => () - | (ERROR,SOME src) => loop src (* message already given *) - | (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop src) - | (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop src) (* usually *) - | (e,SOME src) => (error (Toplevel.exn_message e); loop src) + | (ERROR,SOME src) => loop true src (* message already given *) + | (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop true src) + | (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop true src) (* usually *) + | (e,SOME src) => (error (Toplevel.exn_message e); loop true src) | (_,NONE) => () in (* NB: simple tty for now; later might read from other tty-style sources (e.g. sockets). *) @@ -1344,7 +1362,7 @@ val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty) - val pgip_toplevel = loop + val pgip_toplevel = loop true end @@ -1422,7 +1440,8 @@ sync_thy_loader (); print_mode := proof_generalN :: (! print_mode \ proof_generalN); if pgip then - print_mode := pgmlN :: (pgmlatomsN :: (! print_mode \ pgmlN \ pgmlatomsN)) + (init_pgip_session_id(); + print_mode := pgmlN :: (pgmlatomsN :: (! print_mode \ pgmlN \ pgmlatomsN))) else pgip_emacs_compatibility_flag := true; (* assume this for PG <3.6 compatibility *) set quick_and_dirty;