equal
deleted
inserted
replaced
463 Scan.repeat (parse_spass_pirate_dependency --| Scan.option ($$ "," || $$ " ")) x |
463 Scan.repeat (parse_spass_pirate_dependency --| Scan.option ($$ "," || $$ " ")) x |
464 fun parse_spass_pirate_file_source x = |
464 fun parse_spass_pirate_file_source x = |
465 ((Scan.this_string "Input" || Scan.this_string "Conj") |-- $$ "(" |-- scan_general_id |
465 ((Scan.this_string "Input" || Scan.this_string "Conj") |-- $$ "(" |-- scan_general_id |
466 --| $$ ")") x |
466 --| $$ ")") x |
467 fun parse_spass_pirate_inference_source x = |
467 fun parse_spass_pirate_inference_source x = |
468 (scan_general_id |-- $$ "(" -- parse_spass_pirate_dependencies --| $$ ")") x |
468 (scan_general_id -- ($$ "(" |-- parse_spass_pirate_dependencies --| $$ ")")) x |
469 fun parse_spass_pirate_source x = |
469 fun parse_spass_pirate_source x = |
470 (parse_spass_pirate_file_source >> (fn s => File_Source ("", SOME s)) |
470 (parse_spass_pirate_file_source >> (fn s => File_Source ("", SOME s)) |
471 || parse_spass_pirate_inference_source >> Inference_Source) x |
471 || parse_spass_pirate_inference_source >> Inference_Source) x |
472 |
472 |
473 (* Syntax: <num> <stuff> || <atoms> -> <atoms> . origin\(<origin>\) *) |
473 (* Syntax: <num> <stuff> || <atoms> -> <atoms> . origin\(<origin>\) *) |