equal
deleted
inserted
replaced
29 type message |
29 type message |
30 val to_string: T -> string |
30 val to_string: T -> string |
31 val single_to_string: single -> string |
31 val single_to_string: single -> string |
32 val single_empty: single |
32 val single_empty: single |
33 |
33 |
34 val init: theory -> Formalise.model -> Model_Pattern.T -> T |
34 val init: theory -> Formalise.model -> Model_Pattern.T -> T * Proof.context |
35 val init_PIDE: theory -> Formalise.model -> Model_Pattern.T -> T * Proof.context |
|
36 val values : T -> term list |
35 val values : T -> term list |
37 val values': Proof.context -> T -> Formalise.model * term list |
36 val values': Proof.context -> T -> Formalise.model * term list |
38 val complete_for: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context |
37 val complete_for: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context |
39 val associate_input: Proof.context -> m_field(*del?*) -> descriptor * values -> T -> message * single * values |
38 val associate_input: Proof.context -> m_field(*del?*) -> descriptor * values -> T -> message * single * values |
40 val associate_input': Proof.context -> m_field -> values -> T -> message * single * values |
39 val associate_input': Proof.context -> m_field -> values -> T -> message * single * values |
161 | add n (x :: xs) = (n, x) :: add (n + 1) xs; |
160 | add n (x :: xs) = (n, x) :: add (n + 1) xs; |
162 in add 1 xs end; |
161 in add 1 xs end; |
163 |
162 |
164 fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e); |
163 fun flattup (a, (b, (c, d, e))) = (a, b, c, d, e); |
165 |
164 |
166 fun init _ [] _ = [] |
165 fun init _ [] _ = ([], ContextC.empty) |
167 | init thy fmz pbt = |
166 | init thy fmz pbt = |
168 let |
|
169 val model = |
|
170 (map (fn str => str |
|
171 |> TermC.parseNEW'' thy |
|
172 |> Input_Descript.split |
|
173 |> add_field thy pbt) fmz) |
|
174 |> add_variants; |
|
175 val maxv = model |> map fst |> max_variant; |
|
176 val maxv = if maxv = 0 then 1 else maxv; |
|
177 val model' = model |
|
178 |> collect_variants |
|
179 |> map (replace_0 maxv |> apfst) |
|
180 |> add_enumerate |
|
181 |> map flattup; |
|
182 in model' end; |
|
183 fun init_PIDE _ [] _ = ([], ContextC.empty) |
|
184 | init_PIDE thy fmz pbt = |
|
185 let |
167 let |
186 val (ts, ctxt) = ContextC.build_while_parsing fmz thy |
168 val (ts, ctxt) = ContextC.build_while_parsing fmz thy |
187 val model = |
169 val model = |
188 (map (fn t => t |
170 (map (fn t => t |
189 |> Input_Descript.split |
171 |> Input_Descript.split |