src/Pure/PIDE/markup.scala
changeset 56864 0446c7ac2e32
parent 56843 b2bfcd8cda80
child 57594 037f3b251df5
equal deleted inserted replaced
56863:5fdb61a9a010 56864:0446c7ac2e32
   457           ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok))
   457           ("id", id), ("ok", Properties.Value.Boolean(ok))) => Some((id, ok))
   458         case _ => None
   458         case _ => None
   459       }
   459       }
   460   }
   460   }
   461 
   461 
       
   462   val PRINT_OPERATIONS = "print_operations"
       
   463 
   462 
   464 
   463   /* simplifier trace */
   465   /* simplifier trace */
   464 
   466 
   465   val SIMP_TRACE = "simp_trace"
   467   val SIMP_TRACE = "simp_trace"
   466 
   468