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 in map parse_solution (Library.trim_split_lines sol) end |
868 in map parse_solution (split_lines sol) end |
869 |
869 |
870 |
870 |
871 (* calling external interpreter and getting results *) |
871 (* calling external interpreter and getting results *) |
872 |
872 |
873 fun run ctxt p (query_rel, args) vnames nsols = |
873 fun run ctxt p (query_rel, args) vnames nsols = |