44 val exn_message: exn -> string |
44 val exn_message: exn -> string |
45 val program: (unit -> 'a) -> 'a |
45 val program: (unit -> 'a) -> 'a |
46 type transition |
46 type transition |
47 val undo_limit: bool -> int option |
47 val undo_limit: bool -> int option |
48 val empty: transition |
48 val empty: transition |
49 val name_of: transition -> string |
|
50 val source_of: transition -> OuterLex.token list option |
|
51 val name: string -> transition -> transition |
49 val name: string -> transition -> transition |
52 val position: Position.T -> transition -> transition |
50 val position: Position.T -> transition -> transition |
53 val source: OuterLex.token list -> transition -> transition |
|
54 val interactive: bool -> transition -> transition |
51 val interactive: bool -> transition -> transition |
55 val print: transition -> transition |
52 val print: transition -> transition |
56 val print': string -> transition -> transition |
|
57 val three_buffersN: string |
|
58 val print3: transition -> transition |
|
59 val no_timing: transition -> transition |
53 val no_timing: transition -> transition |
60 val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit) -> |
54 val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit) -> |
61 transition -> transition |
55 transition -> transition |
62 val init_empty: (state -> bool) -> (unit -> unit) -> transition -> transition |
56 val init_empty: (state -> bool) -> (unit -> unit) -> transition -> transition |
63 val exit: transition -> transition |
57 val exit: transition -> transition |
431 |
425 |
432 |
426 |
433 (* datatype transition *) |
427 (* datatype transition *) |
434 |
428 |
435 datatype transition = Transition of |
429 datatype transition = Transition of |
436 {name: string, (*command name*) |
430 {name: string, (*command name*) |
437 pos: Position.T, (*source position*) |
431 pos: Position.T, (*source position*) |
438 source: OuterLex.token list option, (*source text*) |
432 int_only: bool, (*interactive-only*) |
439 int_only: bool, (*interactive-only*) |
433 print: bool, (*print result state*) |
440 print: string list, (*print modes (union)*) |
434 no_timing: bool, (*suppress timing*) |
441 no_timing: bool, (*suppress timing*) |
435 trans: trans list}; (*primitive transitions (union)*) |
442 trans: trans list}; (*primitive transitions (union)*) |
436 |
443 |
437 fun make_transition (name, pos, int_only, print, no_timing, trans) = |
444 fun make_transition (name, pos, source, int_only, print, no_timing, trans) = |
438 Transition {name = name, pos = pos, int_only = int_only, print = print, no_timing = no_timing, |
445 Transition {name = name, pos = pos, source = source, |
439 trans = trans}; |
446 int_only = int_only, print = print, no_timing = no_timing, trans = trans}; |
440 |
447 |
441 fun map_transition f (Transition {name, pos, int_only, print, no_timing, trans}) = |
448 fun map_transition f (Transition {name, pos, source, int_only, print, no_timing, trans}) = |
442 make_transition (f (name, pos, int_only, print, no_timing, trans)); |
449 make_transition (f (name, pos, source, int_only, print, no_timing, trans)); |
443 |
450 |
444 val empty = make_transition ("<unknown>", Position.none, false, false, false, []); |
451 val empty = make_transition ("<unknown>", Position.none, NONE, false, [], false, []); |
|
452 |
|
453 fun name_of (Transition {name, ...}) = name; |
|
454 fun source_of (Transition {source, ...}) = source; |
|
455 |
445 |
456 |
446 |
457 (* diagnostics *) |
447 (* diagnostics *) |
458 |
448 |
459 fun str_of_transition (Transition {name, pos, ...}) = quote name ^ Position.str_of pos; |
449 fun str_of_transition (Transition {name, pos, ...}) = quote name ^ Position.str_of pos; |
465 ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state); |
455 ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state); |
466 |
456 |
467 |
457 |
468 (* modify transitions *) |
458 (* modify transitions *) |
469 |
459 |
470 fun name nm = map_transition (fn (_, pos, source, int_only, print, no_timing, trans) => |
460 fun name nm = map_transition (fn (_, pos, int_only, print, no_timing, trans) => |
471 (nm, pos, source, int_only, print, no_timing, trans)); |
461 (nm, pos, int_only, print, no_timing, trans)); |
472 |
462 |
473 fun position pos = map_transition (fn (name, _, source, int_only, print, no_timing, trans) => |
463 fun position pos = map_transition (fn (name, _, int_only, print, no_timing, trans) => |
474 (name, pos, source, int_only, print, no_timing, trans)); |
464 (name, pos, int_only, print, no_timing, trans)); |
475 |
465 |
476 fun source src = map_transition (fn (name, pos, _, int_only, print, no_timing, trans) => |
466 fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, trans) => |
477 (name, pos, SOME src, int_only, print, no_timing, trans)); |
467 (name, pos, int_only, print, no_timing, trans)); |
478 |
468 |
479 fun interactive int_only = map_transition (fn (name, pos, source, _, print, no_timing, trans) => |
469 val no_timing = map_transition (fn (name, pos, int_only, print, _, trans) => |
480 (name, pos, source, int_only, print, no_timing, trans)); |
470 (name, pos, int_only, print, true, trans)); |
481 |
471 |
482 val no_timing = map_transition (fn (name, pos, source, int_only, print, _, trans) => |
472 fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, trans) => |
483 (name, pos, source, int_only, print, true, trans)); |
473 (name, pos, int_only, print, no_timing, trans @ [tr])); |
484 |
474 |
485 fun add_trans tr = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) => |
475 val print = map_transition (fn (name, pos, int_only, _, no_timing, trans) => |
486 (name, pos, source, int_only, print, no_timing, trans @ [tr])); |
476 (name, pos, int_only, true, no_timing, trans)); |
487 |
|
488 fun print' mode = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) => |
|
489 (name, pos, source, int_only, insert (op =) mode print, no_timing, trans)); |
|
490 |
|
491 val print = print' ""; |
|
492 |
|
493 val three_buffersN = "three_buffers"; |
|
494 val print3 = print' three_buffersN; |
|
495 |
477 |
496 |
478 |
497 (* basic transitions *) |
479 (* basic transitions *) |
498 |
480 |
499 fun init_theory f exit kill = add_trans (Init (f, (exit, kill))); |
481 fun init_theory f exit kill = add_trans (Init (f, (exit, kill))); |
655 local |
637 local |
656 |
638 |
657 fun app int (tr as Transition {trans, pos, int_only, print, no_timing, ...}) = |
639 fun app int (tr as Transition {trans, pos, int_only, print, no_timing, ...}) = |
658 setmp_thread_position tr (fn state => |
640 setmp_thread_position tr (fn state => |
659 let |
641 let |
660 val _ = |
642 val _ = if not int andalso int_only then warning (command_msg "Interactive-only " tr) else (); |
661 if not int andalso int_only then warning (command_msg "Interactive-only " tr) |
|
662 else (); |
|
663 |
643 |
664 fun do_timing f x = (warning (command_msg "" tr); timeap f x); |
644 fun do_timing f x = (warning (command_msg "" tr); timeap f x); |
665 fun do_profiling f x = profile (! profiling) f x; |
645 fun do_profiling f x = profile (! profiling) f x; |
666 |
646 |
667 val (result, status) = |
647 val (result, status) = |
668 state |> (apply_trans int pos trans |
648 state |> (apply_trans int pos trans |
669 |> (if ! profiling > 0 andalso not no_timing then do_profiling else I) |
649 |> (if ! profiling > 0 andalso not no_timing then do_profiling else I) |
670 |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I)); |
650 |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I)); |
671 val _ = |
651 |
672 if int andalso not (! quiet) andalso exists (member (op =) print) ("" :: print_mode_value ()) |
652 val _ = if int andalso not (! quiet) andalso print then print_state false result else (); |
673 then print_state false result else (); |
|
674 |
|
675 in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end); |
653 in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end); |
676 |
654 |
677 in |
655 in |
678 |
656 |
679 fun transition int tr st = |
657 fun transition int tr st = |