equal
deleted
inserted
replaced
7 \<open>fn intree => |
7 \<open>fn intree => |
8 (let |
8 (let |
9 val (calcid, cterm') = case intree of |
9 val (calcid, cterm') = case intree of |
10 XML.Elem (("APPENDFORMULA", []), [ |
10 XML.Elem (("APPENDFORMULA", []), [ |
11 XML.Elem (("CALCID", []), [XML.Text ci]), |
11 XML.Elem (("CALCID", []), [XML.Text ci]), |
12 form]) => (ci |> TermC.int_of_str, form |> xml_to_term_NEW |> term2str) |
12 form]) => (ci |> TermC.int_of_str, form |> xml_to_term_NEW |> Celem.term2str) |
13 | x => raise ERROR ("append_form: WRONG intree = " ^ xmlstr 0 x) |
13 | x => raise ERROR ("append_form: WRONG intree = " ^ xmlstr 0 x) |
14 val result = Kernel.appendFormula calcid cterm' |
14 val result = Kernel.appendFormula calcid cterm' |
15 in result end) |
15 in result end) |
16 handle ERROR msg => appendformulaERROR2xml 4711 msg\<close> |
16 handle ERROR msg => appendformulaERROR2xml 4711 msg\<close> |
17 |
17 |
548 action = (fn intree => |
548 action = (fn intree => |
549 (let |
549 (let |
550 val (calcid, cterm') = case intree of |
550 val (calcid, cterm') = case intree of |
551 XML.Elem (("REPLACEFORMULA", []), [ |
551 XML.Elem (("REPLACEFORMULA", []), [ |
552 XML.Elem (("CALCID", []), [XML.Text ci]), form]) |
552 XML.Elem (("CALCID", []), [XML.Text ci]), form]) |
553 => (ci |> TermC.int_of_str, form |> xml_to_term_NEW |> term2str) |
553 => (ci |> TermC.int_of_str, form |> xml_to_term_NEW |> Celem.term2str) |
554 | tree => raise ERROR ("replace_form: WRONG intree = " ^ xmlstr 0 tree) |
554 | tree => raise ERROR ("replace_form: WRONG intree = " ^ xmlstr 0 tree) |
555 val result = Kernel.replaceFormula calcid cterm' |
555 val result = Kernel.replaceFormula calcid cterm' |
556 in result end) |
556 in result end) |
557 handle ERROR msg => sysERROR2xml 4711 msg)}\<close> |
557 handle ERROR msg => sysERROR2xml 4711 msg)}\<close> |
558 |
558 |