equal
deleted
inserted
replaced
863 fun dest_eq s = |
863 fun dest_eq s = |
864 (case space_explode "=" s of |
864 (case space_explode "=" s of |
865 (l :: r :: []) => parse_term (unprefix " " r) |
865 (l :: r :: []) => parse_term (unprefix " " r) |
866 | _ => raise Fail "unexpected equation in prolog output") |
866 | _ => raise Fail "unexpected equation in prolog output") |
867 fun parse_solution s = map dest_eq (space_explode ";" s) |
867 fun parse_solution s = map dest_eq (space_explode ";" s) |
868 val sols = (case Library.trim_split_lines sol of [] => [] | s => fst (split_last s)) |
868 in map parse_solution (Library.trim_split_lines sol) end |
869 in |
|
870 map parse_solution sols |
|
871 end |
|
872 |
869 |
873 |
870 |
874 (* calling external interpreter and getting results *) |
871 (* calling external interpreter and getting results *) |
875 |
872 |
876 fun run ctxt p (query_rel, args) vnames nsols = |
873 fun run ctxt p (query_rel, args) vnames nsols = |