equal
deleted
inserted
replaced
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 |
|
35 val init_PIDE: theory -> Formalise.model -> Model_Pattern.T -> T * Proof.context |
35 val values : T -> term list |
36 val values : T -> term list |
36 val values': Proof.context -> T -> Formalise.model * term list |
37 val values': Proof.context -> T -> Formalise.model * term list |
37 val complete_for: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context |
38 val complete_for: Model_Pattern.T -> T -> T * Proof.context -> T * Proof.context |
38 val associate_input: Proof.context -> m_field(*del?*) -> descriptor * values -> T -> message * single * values |
39 val associate_input: Proof.context -> m_field(*del?*) -> descriptor * values -> T -> message * single * values |
39 val associate_input': Proof.context -> m_field -> values -> T -> message * single * values |
40 val associate_input': Proof.context -> m_field -> values -> T -> message * single * values |
177 |> collect_variants |
178 |> collect_variants |
178 |> map (replace_0 maxv |> apfst) |
179 |> map (replace_0 maxv |> apfst) |
179 |> add_enumerate |
180 |> add_enumerate |
180 |> map flattup; |
181 |> map flattup; |
181 in model' end; |
182 in model' end; |
182 |
183 fun init_PIDE _ [] _ = ([], ContextC.empty) |
|
184 | init_PIDE thy fmz pbt = |
|
185 let |
|
186 val (ts, ctxt) = ContextC.build_while_parsing fmz thy |
|
187 val model = |
|
188 (map (fn t => t |
|
189 |> Input_Descript.split |
|
190 |> add_field thy pbt) ts) |
|
191 |> add_variants; |
|
192 val maxv = model |> map fst |> max_variant; |
|
193 val maxv = if maxv = 0 then 1 else maxv; |
|
194 val model' = model |
|
195 |> collect_variants |
|
196 |> map (replace_0 maxv |> apfst) |
|
197 |> add_enumerate |
|
198 |> map flattup |
|
199 in (model', ctxt) end |
183 |
200 |
184 (** get the values **) |
201 (** get the values **) |
185 |
202 |
186 fun mkval _(*dsc*) [] = raise ERROR "mkval called with []" |
203 fun mkval _(*dsc*) [] = raise ERROR "mkval called with []" |
187 | mkval _ [t] = t |
204 | mkval _ [t] = t |