equal
deleted
inserted
replaced
7 signature REFERENCES = |
7 signature REFERENCES = |
8 sig |
8 sig |
9 type T |
9 type T |
10 val empty: T |
10 val empty: T |
11 val to_string: T -> string |
11 val to_string: T -> string |
12 val select : T -> T -> T |
12 val select_input : T -> T -> T |
13 |
13 |
14 val complete: Ctree.state -> Ctree.state |
14 val complete: Ctree.state -> Ctree.state |
15 val are_complete: Ctree.state -> bool |
15 val are_complete: Ctree.state -> bool |
16 end |
16 end |
17 |
17 |
22 |
22 |
23 type id = References_Def.id; |
23 type id = References_Def.id; |
24 type T = References_Def.T; |
24 type T = References_Def.T; |
25 val empty = References_Def.empty; |
25 val empty = References_Def.empty; |
26 val to_string = References_Def.to_string; |
26 val to_string = References_Def.to_string; |
27 val select = References_Def.select; |
27 val select_input = References_Def.select_input; |
28 |
28 |
29 (* have (thy, pbl, met) _all_ been specified explicitly ? *) |
29 (* have (thy, pbl, met) _all_ been specified explicitly ? *) |
30 fun are_complete (pt, pos as (p, _)) = |
30 fun are_complete (pt, pos as (p, _)) = |
31 if (not o Ctree.is_pblobj o (Ctree.get_obj I pt)) p then |
31 if (not o Ctree.is_pblobj o (Ctree.get_obj I pt)) p then |
32 raise ERROR ("References.is_complete: called by PrfObj at " ^ Pos.pos'2str pos) |
32 raise ERROR ("References.is_complete: called by PrfObj at " ^ Pos.pos'2str pos) |
41 fun complete (pt, pos as (p, _)) = |
41 fun complete (pt, pos as (p, _)) = |
42 let |
42 let |
43 val (ospec, spec) = case Ctree.get_obj I pt p of |
43 val (ospec, spec) = case Ctree.get_obj I pt p of |
44 Ctree.PblObj {origin = (_, ospec, _), spec, ...} => (ospec, spec) |
44 Ctree.PblObj {origin = (_, ospec, _), spec, ...} => (ospec, spec) |
45 | _ => raise ERROR "References.complete: uncovered case get_obj" |
45 | _ => raise ERROR "References.complete: uncovered case get_obj" |
46 val pt = Ctree.update_spec pt p (select ospec spec) |
46 val pt = Ctree.update_spec pt p (select_input ospec spec) |
47 in |
47 in |
48 (pt, pos) |
48 (pt, pos) |
49 end |
49 end |
50 |
50 |
51 (**)end(**) |
51 (**)end(**) |