1 theory syntaxe imports Main begin
3 section {* Old parsing *}
4 text {* Old parsing in ISAC used theories *}
7 fun parse thy str = Syntax.read_term_global thy str;
9 [(parse thy "equ::bool", parse thy "x + (1::int) = 2"),
10 (parse thy "var::int", parse thy "x::int"),
11 (parse thy "sol::bool", parse thy "(x::int) = 1")
13 val precond = parse thy "(0::int) < x"
15 text {* However, user input could not be parsed ...*}
16 ML {* parse thy "x = 2 - 1" *}
17 text {* ... because the type 'int' is lost (we have type 'a now).
18 The learner would need to input x::int all the time. *}
20 section {* Contexts *}
22 val ctxt = ProofContext.init_global thy;
24 (*... prepare ctxt ...*)
26 fun parseNEW ctxt str = Syntax.read_term ctxt str;
29 section {* New parsing *}
30 text {* New parsing in ISAC uses contexts, which are rigorously updated
31 by the Lucas-Interpreter. Then ...*}
32 ML {* parse thy "x = 2 - 1" *}
33 text {* ... x gets type 'int' from the context. *}