src/Doc/antiquote_setup.ML
changeset 59067 dd8ec9138112
parent 59066 45ab32a542fe
child 59082 25501ba956ac
     1.1 --- a/src/Doc/antiquote_setup.ML	Sun Nov 30 13:15:04 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Sun Nov 30 14:02:48 2014 +0100
     1.3 @@ -37,28 +37,29 @@
     1.4  
     1.5  local
     1.6  
     1.7 -val ml_toks = ML_Lex.read Position.none;
     1.8 +fun ml_val (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read ");"
     1.9 +  | ml_val (toks1, toks2) =
    1.10 +      ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
    1.11  
    1.12 -fun ml_val (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks ");"
    1.13 -  | ml_val (toks1, toks2) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");";
    1.14 -
    1.15 -fun ml_op (toks1, []) = ml_toks "fn _ => (op " @ toks1 @ ml_toks ");"
    1.16 -  | ml_op (toks1, toks2) = ml_toks "fn _ => (op " @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");";
    1.17 +fun ml_op (toks1, []) = ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read ");"
    1.18 +  | ml_op (toks1, toks2) =
    1.19 +      ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");";
    1.20  
    1.21 -fun ml_type (toks1, []) = ml_toks "val _ = NONE : (" @ toks1 @ ml_toks ") option;"
    1.22 +fun ml_type (toks1, []) = ML_Lex.read "val _ = NONE : (" @ toks1 @ ML_Lex.read ") option;"
    1.23    | ml_type (toks1, toks2) =
    1.24 -      ml_toks "val _ = [NONE : (" @ toks1 @ ml_toks ") option, NONE : (" @
    1.25 -        toks2 @ ml_toks ") option];";
    1.26 +      ML_Lex.read "val _ = [NONE : (" @ toks1 @ ML_Lex.read ") option, NONE : (" @
    1.27 +        toks2 @ ML_Lex.read ") option];";
    1.28  
    1.29 -fun ml_exception (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);"
    1.30 +fun ml_exception (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : exn);"
    1.31    | ml_exception (toks1, toks2) =
    1.32 -      ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks " -> exn);";
    1.33 +      ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read " -> exn);";
    1.34  
    1.35  fun ml_structure (toks, _) =
    1.36 -  ml_toks "functor XXX() = struct structure XX = " @ toks @ ml_toks " end;";
    1.37 +  ML_Lex.read "functor XXX() = struct structure XX = " @ toks @ ML_Lex.read " end;";
    1.38  
    1.39  fun ml_functor (Antiquote.Text tok :: _, _) =
    1.40 -      ml_toks "ML_Env.check_functor " @ ml_toks (ML_Syntax.print_string (ML_Lex.content_of tok))
    1.41 +      ML_Lex.read "ML_Env.check_functor " @
    1.42 +      ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok))
    1.43    | ml_functor _ = raise Fail "Bad ML functor specification";
    1.44  
    1.45  val is_name = ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.LongIdent);