1.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon May 31 19:36:13 2010 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon May 31 21:06:57 2010 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  sig
     1.5    val command: string -> string -> Keyword.T ->
     1.6      (Toplevel.transition -> Toplevel.transition) parser -> unit
     1.7 -  val markup_command: ThyOutput.markup -> string -> string -> Keyword.T ->
     1.8 +  val markup_command: Thy_Output.markup -> string -> string -> Keyword.T ->
     1.9      (Toplevel.transition -> Toplevel.transition) parser -> unit
    1.10    val improper_command: string -> string -> Keyword.T ->
    1.11      (Toplevel.transition -> Toplevel.transition) parser -> unit
    1.12 @@ -43,7 +43,7 @@
    1.13  
    1.14  datatype command = Command of
    1.15   {comment: string,
    1.16 -  markup: ThyOutput.markup option,
    1.17 +  markup: Thy_Output.markup option,
    1.18    int_only: bool,
    1.19    parse: (Toplevel.transition -> Toplevel.transition) parser};
    1.20  
    1.21 @@ -83,7 +83,7 @@
    1.22  local
    1.23  
    1.24  val global_commands = Unsynchronized.ref (Symtab.empty: command Symtab.table);
    1.25 -val global_markups = Unsynchronized.ref ([]: (string * ThyOutput.markup) list);
    1.26 +val global_markups = Unsynchronized.ref ([]: (string * Thy_Output.markup) list);
    1.27  
    1.28  fun change_commands f = CRITICAL (fn () =>
    1.29   (Unsynchronized.change global_commands f;
    1.30 @@ -235,9 +235,9 @@
    1.31  
    1.32  fun prepare_span commands span =
    1.33    let
    1.34 -    val range_pos = Position.encode_range (ThySyntax.span_range span);
    1.35 -    val toks = ThySyntax.span_content span;
    1.36 -    val _ = List.app ThySyntax.report_token toks;
    1.37 +    val range_pos = Position.encode_range (Thy_Syntax.span_range span);
    1.38 +    val toks = Thy_Syntax.span_content span;
    1.39 +    val _ = List.app Thy_Syntax.report_token toks;
    1.40    in
    1.41      (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
    1.42        [tr] => (tr, true)
    1.43 @@ -257,7 +257,7 @@
    1.44  
    1.45  fun prepare_command pos str =
    1.46    let val (lexs, commands) = get_syntax () in
    1.47 -    (case ThySyntax.parse_spans lexs pos str of
    1.48 +    (case Thy_Syntax.parse_spans lexs pos str of
    1.49        [span] => #1 (prepare_span commands span)
    1.50      | _ => Toplevel.malformed pos not_singleton)
    1.51    end;
    1.52 @@ -271,21 +271,21 @@
    1.53  
    1.54      val _ = Present.init_theory name;
    1.55  
    1.56 -    val toks = Source.exhausted (ThySyntax.token_source lexs pos (Source.of_list text));
    1.57 -    val spans = Source.exhaust (ThySyntax.span_source toks);
    1.58 -    val _ = List.app ThySyntax.report_span spans;
    1.59 -    val units = Source.exhaust (ThySyntax.unit_source (Source.of_list spans))
    1.60 +    val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_list text));
    1.61 +    val spans = Source.exhaust (Thy_Syntax.span_source toks);
    1.62 +    val _ = List.app Thy_Syntax.report_span spans;
    1.63 +    val units = Source.exhaust (Thy_Syntax.unit_source (Source.of_list spans))
    1.64        |> maps (prepare_unit commands);
    1.65  
    1.66      val _ = Present.theory_source name
    1.67 -      (fn () => HTML.html_mode (implode o map ThySyntax.present_span) spans);
    1.68 +      (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
    1.69  
    1.70      val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
    1.71      val results = cond_timeit time "" (fn () => Toplevel.excursion units);
    1.72      val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
    1.73  
    1.74      fun after_load () =
    1.75 -      ThyOutput.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
    1.76 +      Thy_Output.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
    1.77        |> Buffer.content
    1.78        |> Present.theory_output name;
    1.79    in after_load end;