src/Pure/variable.ML
changeset 45472 2046f8e2ecd7
parent 45454 388fb71623dd
child 45650 d314a4e8038f
equal deleted inserted replaced
45471:489f27dcc0f4 45472:2046f8e2ecd7
   295 fun is_fixed ctxt x = can (Name_Space.the_entry (fixes_space ctxt)) x;
   295 fun is_fixed ctxt x = can (Name_Space.the_entry (fixes_space ctxt)) x;
   296 fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
   296 fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
   297 
   297 
   298 val fixed_ord = Name_Space.entry_ord o fixes_space;
   298 val fixed_ord = Name_Space.entry_ord o fixes_space;
   299 val intern_fixed = Name_Space.intern o fixes_space;
   299 val intern_fixed = Name_Space.intern o fixes_space;
   300 val markup_fixed = Name_Space.markup o fixes_space;
       
   301 
   300 
   302 fun lookup_fixed ctxt x =
   301 fun lookup_fixed ctxt x =
   303   let val x' = intern_fixed ctxt x
   302   let val x' = intern_fixed ctxt x
   304   in if is_fixed ctxt x' then SOME x' else NONE end;
   303   in if is_fixed ctxt x' then SOME x' else NONE end;
   305 
   304 
   306 fun revert_fixed ctxt x =
   305 fun revert_fixed ctxt x =
   307   (case Symtab.lookup (#2 (fixes_of ctxt)) x of
   306   (case Symtab.lookup (#2 (fixes_of ctxt)) x of
   308     SOME x' => if intern_fixed ctxt x' = x then x' else x
   307     SOME x' => if intern_fixed ctxt x' = x then x' else x
   309   | NONE => x);
   308   | NONE => x);
       
   309 
       
   310 fun markup_fixed ctxt x =
       
   311   Name_Space.markup (fixes_space ctxt) x
       
   312   |> Markup.name (revert_fixed ctxt x);
   310 
   313 
   311 fun dest_fixes ctxt =
   314 fun dest_fixes ctxt =
   312   let val (space, tab) = fixes_of ctxt
   315   let val (space, tab) = fixes_of ctxt
   313   in sort (Name_Space.entry_ord space o pairself #2) (map swap (Symtab.dest tab)) end;
   316   in sort (Name_Space.entry_ord space o pairself #2) (map swap (Symtab.dest tab)) end;
   314 
   317