src/Pure/Thy/thy_output.ML
changeset 36754 403585a89772
parent 36446 06081e4921d6
child 36950 75b8f26f2f07
equal deleted inserted replaced
36753:6e1f3d609a68 36754:403585a89772
   426   ("eta_contract", setmp_CRITICAL Syntax.eta_contract o boolean),
   426   ("eta_contract", setmp_CRITICAL Syntax.eta_contract o boolean),
   427   ("display", setmp_CRITICAL display o boolean),
   427   ("display", setmp_CRITICAL display o boolean),
   428   ("break", setmp_CRITICAL break o boolean),
   428   ("break", setmp_CRITICAL break o boolean),
   429   ("quotes", setmp_CRITICAL quotes o boolean),
   429   ("quotes", setmp_CRITICAL quotes o boolean),
   430   ("mode", fn s => fn f => PrintMode.with_modes [s] f),
   430   ("mode", fn s => fn f => PrintMode.with_modes [s] f),
   431   ("margin", Pretty.setmp_margin_CRITICAL o integer),
   431   ("margin", setmp_CRITICAL Pretty.margin_default o integer),
   432   ("indent", setmp_CRITICAL indent o integer),
   432   ("indent", setmp_CRITICAL indent o integer),
   433   ("source", setmp_CRITICAL source o boolean),
   433   ("source", setmp_CRITICAL source o boolean),
   434   ("goals_limit", setmp_CRITICAL goals_limit o integer)];
   434   ("goals_limit", setmp_CRITICAL goals_limit o integer)];
   435 
   435 
   436 
   436