311 (* parameter table *) |
311 (* parameter table *) |
312 (* ------------------------------------------------------------------------- *) |
312 (* ------------------------------------------------------------------------- *) |
313 |
313 |
314 (* (string * string) -> theory -> theory *) |
314 (* (string * string) -> theory -> theory *) |
315 |
315 |
316 fun set_default_param (name, value) thy = |
316 fun set_default_param (name, value) = RefuteData.map |
317 let |
317 (fn {interpreters, printers, parameters} => |
318 val {interpreters, printers, parameters} = RefuteData.get thy |
|
319 in |
|
320 RefuteData.put (case Symtab.lookup parameters name of |
|
321 NONE => |
|
322 {interpreters = interpreters, printers = printers, |
318 {interpreters = interpreters, printers = printers, |
323 parameters = Symtab.extend (parameters, [(name, value)])} |
319 parameters = Symtab.update (name, value) parameters}); |
324 | SOME _ => |
|
325 {interpreters = interpreters, printers = printers, |
|
326 parameters = Symtab.update (name, value) parameters}) thy |
|
327 end; |
|
328 |
320 |
329 (* ------------------------------------------------------------------------- *) |
321 (* ------------------------------------------------------------------------- *) |
330 (* get_default_param: retrieves the value associated with 'name' from *) |
322 (* get_default_param: retrieves the value associated with 'name' from *) |
331 (* RefuteData's parameter table *) |
323 (* RefuteData's parameter table *) |
332 (* ------------------------------------------------------------------------- *) |
324 (* ------------------------------------------------------------------------- *) |