src/Pure/Thy/thy_output.ML
changeset 30367 ee8841b1b981
parent 30317 159bab53b40d
child 30368 1a2a54f910c9
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sun Mar 08 20:31:01 2009 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Mar 08 20:31:54 2009 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4    val indent: int ref
     1.5    val source: bool ref
     1.6    val break: bool ref
     1.7 -  val add_commands: (string * (Args.src -> Toplevel.node option -> string)) list -> unit
     1.8 +  val add_commands: (string * (Args.src -> Toplevel.state -> string)) list -> unit
     1.9    val add_options: (string * (string -> (unit -> string) -> unit -> string)) list -> unit
    1.10    val defined_command: string -> bool
    1.11    val defined_option: string -> bool
    1.12 @@ -19,10 +19,10 @@
    1.13    val boolean: string -> bool
    1.14    val integer: string -> int
    1.15    val args: (Context.generic * Args.T list -> 'a * (Context.generic * Args.T list)) ->
    1.16 -    (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.node option -> string
    1.17 +    (Args.src -> Proof.context -> 'a -> string) -> Args.src -> Toplevel.state -> string
    1.18    datatype markup = Markup | MarkupEnv | Verbatim
    1.19    val modes: string list ref
    1.20 -  val eval_antiquote: Scan.lexicon -> Toplevel.node option -> SymbolPos.text * Position.T -> string
    1.21 +  val eval_antiquote: Scan.lexicon -> Toplevel.state -> SymbolPos.text * Position.T -> string
    1.22    val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
    1.23      (Toplevel.transition * Toplevel.state) list -> (OuterLex.token, 'a) Source.source -> Buffer.T
    1.24    val str_of_source: Args.src -> string
    1.25 @@ -57,7 +57,7 @@
    1.26  local
    1.27  
    1.28  val global_commands =
    1.29 -  ref (Symtab.empty: (Args.src -> Toplevel.node option -> string) Symtab.table);
    1.30 +  ref (Symtab.empty: (Args.src -> Toplevel.state -> string) Symtab.table);
    1.31  
    1.32  val global_options =
    1.33    ref (Symtab.empty: (string -> (unit -> string) -> unit -> string) Symtab.table);
    1.34 @@ -81,7 +81,7 @@
    1.35        NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos)
    1.36      | SOME f =>
    1.37         (Position.report (Markup.doc_antiq name) pos;
    1.38 -        (fn node => f src node handle ERROR msg =>
    1.39 +        (fn state => f src state handle ERROR msg =>
    1.40            cat_error msg ("The error(s) above occurred in document antiquotation: " ^
    1.41              quote name ^ Position.str_of pos))))
    1.42    end;
    1.43 @@ -127,10 +127,10 @@
    1.44  
    1.45  fun syntax scan = Args.context_syntax "document antiquotation" scan;
    1.46  
    1.47 -fun args scan f src node : string =
    1.48 +fun args scan f src state : string =
    1.49    let
    1.50      val loc = if ! locale = "" then NONE else SOME (! locale);
    1.51 -    val (x, ctxt) = syntax scan src (Toplevel.presentation_context node loc);
    1.52 +    val (x, ctxt) = syntax scan src (Toplevel.presentation_context_of state loc);
    1.53    in f src ctxt x end;
    1.54  
    1.55  
    1.56 @@ -153,20 +153,20 @@
    1.57  
    1.58  val modes = ref ([]: string list);
    1.59  
    1.60 -fun eval_antiquote lex node (txt, pos) =
    1.61 +fun eval_antiquote lex state (txt, pos) =
    1.62    let
    1.63      fun expand (Antiquote.Text s) = s
    1.64        | expand (Antiquote.Antiq x) =
    1.65            let val (opts, src) = Antiquote.read_antiq lex antiq x in
    1.66 -            options opts (fn () => command src node) ();  (*preview errors!*)
    1.67 +            options opts (fn () => command src state) ();  (*preview errors!*)
    1.68              PrintMode.with_modes (! modes @ Latex.modes)
    1.69 -              (Output.no_warnings (options opts (fn () => command src node))) ()
    1.70 +              (Output.no_warnings (options opts (fn () => command src state))) ()
    1.71            end
    1.72        | expand (Antiquote.Open _) = ""
    1.73        | expand (Antiquote.Close _) = "";
    1.74      val ants = Antiquote.read (SymbolPos.explode (txt, pos), pos);
    1.75    in
    1.76 -    if is_none node andalso exists Antiquote.is_antiq ants then
    1.77 +    if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then
    1.78        error ("Unknown context -- cannot expand document antiquotations" ^ Position.str_of pos)
    1.79      else implode (map expand ants)
    1.80    end;
    1.81 @@ -187,9 +187,7 @@
    1.82    | VerbatimToken of string * Position.T;
    1.83  
    1.84  fun output_token lex state =
    1.85 -  let
    1.86 -    val eval = eval_antiquote lex (try Toplevel.node_of state)
    1.87 -  in
    1.88 +  let val eval = eval_antiquote lex state in
    1.89      fn NoToken => ""
    1.90       | BasicToken tok => Latex.output_basic tok
    1.91       | MarkupToken (cmd, txt) => Latex.output_markup cmd (eval txt)
    1.92 @@ -511,13 +509,13 @@
    1.93  
    1.94  fun output pretty src ctxt = output_list pretty src ctxt o single;
    1.95  
    1.96 -fun proof_state node =
    1.97 -  (case Option.map Toplevel.proof_node node of
    1.98 -    SOME (SOME prf) => ProofNode.current prf
    1.99 +fun proof_state state =
   1.100 +  (case try Toplevel.proof_of state of
   1.101 +    SOME prf => prf
   1.102    | _ => error "No proof state");
   1.103  
   1.104 -fun output_goals main_goal src node = args (Scan.succeed ()) (output (fn _ => fn _ =>
   1.105 -  Pretty.chunks (Proof.pretty_goals main_goal (proof_state node)))) src node;
   1.106 +fun output_goals main_goal src state = args (Scan.succeed ()) (output (fn _ => fn _ =>
   1.107 +  Pretty.chunks (Proof.pretty_goals main_goal (proof_state state)))) src state;
   1.108  
   1.109  fun ml_val txt = "fn _ => (" ^ txt ^ ");";
   1.110  fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";