src/Pure/Isar/outer_syntax.ML
changeset 22120 8424ef945cb5
parent 22086 cf6019fece63
child 22826 0f4c501a691e
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Fri Jan 19 22:08:28 2007 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Fri Jan 19 22:08:29 2007 +0100
     1.3 @@ -28,7 +28,7 @@
     1.4    type parser
     1.5    val command: string -> string -> OuterKeyword.T ->
     1.6      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
     1.7 -  val markup_command: IsarOutput.markup -> string -> string -> OuterKeyword.T ->
     1.8 +  val markup_command: ThyOutput.markup -> string -> string -> OuterKeyword.T ->
     1.9      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    1.10    val improper_command: string -> string -> OuterKeyword.T ->
    1.11      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    1.12 @@ -62,7 +62,7 @@
    1.13  type parser_fn = token list -> (Toplevel.transition -> Toplevel.transition) * token list;
    1.14  
    1.15  datatype parser =
    1.16 -  Parser of string * (string * OuterKeyword.T * IsarOutput.markup option) * bool * parser_fn;
    1.17 +  Parser of string * (string * OuterKeyword.T * ThyOutput.markup option) * bool * parser_fn;
    1.18  
    1.19  fun parser int_only markup name comment kind parse =
    1.20    Parser (name, (comment, kind, markup), int_only, parse);
    1.21 @@ -104,9 +104,9 @@
    1.22  
    1.23  val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
    1.24  val global_parsers =
    1.25 -  ref (Symtab.empty: (((string * OuterKeyword.T) * (bool * parser_fn)) * IsarOutput.markup option)
    1.26 +  ref (Symtab.empty: (((string * OuterKeyword.T) * (bool * parser_fn)) * ThyOutput.markup option)
    1.27      Symtab.table);
    1.28 -val global_markups = ref ([]: (string * IsarOutput.markup) list);
    1.29 +val global_markups = ref ([]: (string * ThyOutput.markup) list);
    1.30  
    1.31  fun change_lexicons f =
    1.32    let val lexs = f (! global_lexicons) in
    1.33 @@ -142,8 +142,8 @@
    1.34  
    1.35  (* augment syntax *)
    1.36  
    1.37 -fun add_keywords keywords = change_lexicons (apfst (fn lex =>
    1.38 -  (Scan.extend_lexicon lex (map Symbol.explode keywords))));
    1.39 +fun add_keywords keywords =
    1.40 +  change_lexicons (apfst (Scan.extend_lexicon (map Symbol.explode keywords)));
    1.41  
    1.42  fun add_parser (Parser (name, (comment, kind, markup), int_only, parse)) tab =
    1.43   (if not (Symtab.defined tab name) then ()
    1.44 @@ -152,7 +152,7 @@
    1.45  
    1.46  fun add_parsers parsers =
    1.47    (change_parsers (fold add_parser parsers);
    1.48 -    change_lexicons (apsnd (fn lex => Scan.extend_lexicon lex
    1.49 +    change_lexicons (apsnd (Scan.extend_lexicon
    1.50        (map (fn Parser (name, _, _, _) => Symbol.explode name) parsers))));
    1.51  
    1.52  end;
    1.53 @@ -239,7 +239,7 @@
    1.54  
    1.55  (* check_text *)
    1.56  
    1.57 -fun check_text s state = (IsarOutput.eval_antiquote (#1 (get_lexicons ())) state s; ());
    1.58 +fun check_text s state = (ThyOutput.eval_antiquote (#1 (get_lexicons ())) state s; ());
    1.59  
    1.60  
    1.61  (* deps_thy *)
    1.62 @@ -287,7 +287,7 @@
    1.63        |> toplevel_source false false false (K (get_parser ()))
    1.64        |> Source.exhaust;
    1.65    in
    1.66 -    IsarOutput.present_thy (#1 (get_lexicons ())) command_tags is_markup trs toks
    1.67 +    ThyOutput.present_thy (#1 (get_lexicons ())) command_tags is_markup trs toks
    1.68      |> Buffer.content
    1.69      |> Present.theory_output name
    1.70    end;
    1.71 @@ -301,7 +301,7 @@
    1.72        run_thy name path;
    1.73        writeln ("**** Finished theory " ^ quote name ^ " ****\n")))
    1.74    else run_thy name path;
    1.75 -  Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name)));
    1.76 +  ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name)));
    1.77    if ml then try_ml_file name time else ());
    1.78  
    1.79  end;
    1.80 @@ -313,7 +313,7 @@
    1.81  (* main loop *)
    1.82  
    1.83  fun gen_loop term no_pos =
    1.84 - (Context.set_context NONE;
    1.85 + (ML_Context.set_context NONE;
    1.86    Toplevel.loop (isar term no_pos));
    1.87  
    1.88  fun gen_main term no_pos =