429 |
429 |
430 fun proper_inform_file_processed file state = |
430 fun proper_inform_file_processed file state = |
431 let val name = thy_name file in |
431 let val name = thy_name file in |
432 if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then |
432 if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then |
433 (ThyInfo.touch_child_thys name; |
433 (ThyInfo.touch_child_thys name; |
434 transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg => |
434 ThyInfo.pretend_use_thy_only name handle ERROR msg => |
435 (warning msg; warning ("Failed to register theory: " ^ quote name); |
435 (warning msg; warning ("Failed to register theory: " ^ quote name); |
436 tell_file_retracted (Path.base (Path.unpack file)))) |
436 tell_file_retracted (Path.base (Path.unpack file)))) |
437 else raise Toplevel.UNDEF |
437 else raise Toplevel.UNDEF |
438 end; |
438 end; |
439 |
439 |
1300 | SOME id => if (matching_pgip_id id) then |
1300 | SOME id => if (matching_pgip_id id) then |
1301 (List.app process_pgip_element pgips; true) |
1301 (List.app process_pgip_element pgips; true) |
1302 else false |
1302 else false |
1303 end) |
1303 end) |
1304 | _ => raise PGIP "Invalid PGIP packet received") |
1304 | _ => raise PGIP "Invalid PGIP packet received") |
1305 handle (PGIP msg) => |
1305 handle PGIP msg => |
1306 (error (msg ^ "\nPGIP error occured in XML text below:\n" ^ |
1306 error (msg ^ "\nPGIP error occured in XML text below:\n" ^ |
1307 (XML.string_of_tree xml)))) |
1307 (XML.string_of_tree xml))) |
1308 |
1308 |
1309 val process_pgip = K () o process_pgip_tree o XML.tree_of_string |
1309 val process_pgip = K () o process_pgip_tree o XML.tree_of_string |
1310 |
1310 |
1311 end |
1311 end |
1312 |
1312 |
1334 end handle e => handler (e,SOME src) (* i.e. error in ready/XML parse *) |
1334 end handle e => handler (e,SOME src) (* i.e. error in ready/XML parse *) |
1335 |
1335 |
1336 and handler (e,srco) = |
1336 and handler (e,srco) = |
1337 case (e,srco) of |
1337 case (e,srco) of |
1338 (XML_PARSE,SOME src) => |
1338 (XML_PARSE,SOME src) => |
1339 panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *) |
1339 Output.panic "Invalid XML input, aborting" (* NB: loop OK for tty, but want exit on EOF *) |
1340 | (PGIP_QUIT,_) => () |
1340 | (PGIP_QUIT,_) => () |
1341 | (ERROR,SOME src) => loop true src (* message already given *) |
|
1342 | (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop true src) |
1341 | (Interrupt,SOME src) => (!error_fn "Interrupt during PGIP processing"; loop true src) |
1343 | (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop true src) (* usually *) |
1342 | (Toplevel.UNDEF,SOME src) => (error "No working context defined"; loop true src) (* usually *) |
1344 | (e,SOME src) => (error (Toplevel.exn_message e); loop true src) |
1343 | (e,SOME src) => (error (Toplevel.exn_message e); loop true src) |
1345 | (_,NONE) => () |
1344 | (_,NONE) => () |
1346 in |
1345 in |
1439 |
1438 |
1440 fun init isar = |
1439 fun init isar = |
1441 (init_setup isar false; |
1440 (init_setup isar false; |
1442 if isar then Isar.sync_main () else isa_restart ()); |
1441 if isar then Isar.sync_main () else isa_restart ()); |
1443 |
1442 |
1444 fun init_pgip false = panic "PGIP not supported for Isabelle/classic mode." |
1443 fun init_pgip false = Output.panic "PGIP not supported for Isabelle/classic mode." |
1445 | init_pgip true = (init_setup true true; pgip_toplevel tty_src); |
1444 | init_pgip true = (init_setup true true; pgip_toplevel tty_src); |
1446 |
1445 |
1447 |
1446 |
1448 |
1447 |
1449 (** generate elisp file for keyword classification **) |
1448 (** generate elisp file for keyword classification **) |