equal
deleted
inserted
replaced
406 in schedule_tasks tasks end; |
406 in schedule_tasks tasks end; |
407 |
407 |
408 fun use_thy name = |
408 fun use_thy name = |
409 use_theories |
409 use_theories |
410 {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime, |
410 {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime, |
411 qualifier = Resources.default_qualifier (), master_dir = Path.current} |
411 qualifier = Resources.default_qualifier, master_dir = Path.current} |
412 [(name, Position.none)]; |
412 [(name, Position.none)]; |
413 |
413 |
414 |
414 |
415 (* toplevel scripting -- without maintaining database *) |
415 (* toplevel scripting -- without maintaining database *) |
416 |
416 |