src/Pure/PIDE/markup.ML
changeset 62231 25f4a9cd8b68
parent 61864 3a5992c3410c
child 62520 2382876c238b
equal deleted inserted replaced
62230:949d2c9f6ff7 62231:25f4a9cd8b68
    26   val symbolsN: string
    26   val symbolsN: string
    27   val delimitedN: string
    27   val delimitedN: string
    28   val is_delimited: Properties.T -> bool
    28   val is_delimited: Properties.T -> bool
    29   val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T
    29   val language: {name: string, symbols: bool, antiquotes: bool, delimited: bool} -> T
    30   val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T
    30   val language': {name: string, symbols: bool, antiquotes: bool} -> bool -> T
    31   val language_outer: bool -> T
    31   val language_Isar: bool -> T
    32   val language_method: T
    32   val language_method: T
    33   val language_attribute: T
    33   val language_attribute: T
    34   val language_sort: bool -> T
    34   val language_sort: bool -> T
    35   val language_type: bool -> T
    35   val language_type: bool -> T
    36   val language_term: bool -> T
    36   val language_term: bool -> T
   299     (delimitedN, print_bool delimited)]);
   299     (delimitedN, print_bool delimited)]);
   300 
   300 
   301 fun language' {name, symbols, antiquotes} delimited =
   301 fun language' {name, symbols, antiquotes} delimited =
   302   language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited};
   302   language {name = name, symbols = symbols, antiquotes = antiquotes, delimited = delimited};
   303 
   303 
   304 val language_outer = language' {name = "", symbols = true, antiquotes = false};
   304 val language_Isar = language' {name = "Isar", symbols = true, antiquotes = false};
   305 val language_method =
   305 val language_method =
   306   language {name = "method", symbols = true, antiquotes = false, delimited = false};
   306   language {name = "method", symbols = true, antiquotes = false, delimited = false};
   307 val language_attribute =
   307 val language_attribute =
   308   language {name = "attribute", symbols = true, antiquotes = false, delimited = false};
   308   language {name = "attribute", symbols = true, antiquotes = false, delimited = false};
   309 val language_sort = language' {name = "sort", symbols = true, antiquotes = false};
   309 val language_sort = language' {name = "sort", symbols = true, antiquotes = false};